ibi Show Code edit
## Biconditional to Condition <title></div> <div style="margin-left: 40px" class="code">## <summary></div> <div style="margin-left: 40px" class="code">## Inference that converts a biconditional implied by one of its arguments,</div> <div style="margin-left: 40px" class="code">## into an implication.</div> <div style="margin-left: 40px" class="code">## </summary></div> <div style="margin-left: 40px" class="code">thm (ibi () (ibi.1 (-> ph (<-> ph ps))) (-> ph ps) <span class="step">ibi.1</span> <a href="/peano/prop.gh/biimpd"><span class="step">biimpd</span></a> <a href="/peano/prop.gh/pm2.43i"><span class="step">pm2.43i</span></a>)</div> <div style="margin-left: 72px" class="intermediate"><span class="sexp">(-> ph ps)</span></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/ibi" class="end-edit">edit</a>