dfor2 Show Code edit
## Alternative Definition of OR </title</div> <div style="margin-left: 40px" class="code">## <summary> Logical 'or' expressed in terms of implication only. </summary></div> <div style="margin-left: 40px" class="code">thm (dfor2 () () (<-> (\/ ph ps) (-> (-> ph ps) ps))</div> <div style="margin-left: 72px" class="code">ph ps <a href="/peano/prop.gh/df-or"><span class="step">df-or</span></a></div> <div style="margin-left: 72px" class="intermediate"><span class="sexp">(<-> (\/ ph ps) (-> (-. ph) ps))</span></div> <div style="margin-left: 72px" class="code">ph ps <a href="/peano/prop.gh/dfor2-lemma"><span class="step">dfor2-lemma</span></a></div> <div style="margin-left: 104px" class="intermediate"><span class="sexp">(<-> (-> (-. ph) ps) (-> (-> ph ps) ps))</span></div> <div style="margin-left: 72px" class="code"><a href="/peano/prop.gh/bitri"><span class="step">bitri</span></a></div> <div style="margin-left: 72px" class="intermediate"><span class="sexp">(<-> (\/ ph ps) (-> (-> ph ps) ps))</span></div> <div style="margin-left: 40px" class="code">)</div> </div> <script src="/js/verify.js" type="text/javascript"></script> <script type="text/javascript" src="//cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.1/MathJax.js?config=TeX-AMS-MML_HTMLorMML"> </script> <script src="/js/showthm.js" type="text/javascript"></script> <script src="/js/proofstep.js" type="text/javascript"></script> <script src="/js/sexpression.js" type="text/javascript"></script> <script src="/js/prover/numUtil.js" type="text/javascript"></script> <script src="/js/typeset.js" type="text/javascript"></script> <script type="text/javascript"> GH.typeset_intermediates() </script> <a href="/edit/peano/prop.gh/dfor2" class="end-edit">edit</a>