ibd Show Code edit
## Biconditional to Condition <title></div> <div style="margin-left: 40px" class="code">## <summary></div> <div style="margin-left: 40px" class="code">## Deduction 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 (ibd () (ibd.1 (-> ph (-> ps (<-> ps ch)))) (-> ph (-> ps ch)) <span class="step">ibd.1</span> ps ch <a href="/peano/prop.gh/ibib"><span class="step">ibib</span></a> <a href="/peano/prop.gh/sylibr"><span class="step">sylibr</span></a>)</div> <div style="margin-left: 72px" class="intermediate"><span class="sexp">(-> ph (-> ps ch))</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/ibd" class="end-edit">edit</a>