New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  bi1 GIF version

Theorem bi1 178
 Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.)
Assertion
Ref Expression
bi1 ((φψ) → (φψ))

Proof of Theorem bi1
StepHypRef Expression
1 df-bi 177 . . 3 ¬ (((φψ) → ¬ ((φψ) → ¬ (ψφ))) → ¬ (¬ ((φψ) → ¬ (ψφ)) → (φψ)))
2 simplim 143 . . 3 (¬ (((φψ) → ¬ ((φψ) → ¬ (ψφ))) → ¬ (¬ ((φψ) → ¬ (ψφ)) → (φψ))) → ((φψ) → ¬ ((φψ) → ¬ (ψφ))))
31, 2ax-mp 5 . 2 ((φψ) → ¬ ((φψ) → ¬ (ψφ)))
4 simplim 143 . 2 (¬ ((φψ) → ¬ (ψφ)) → (φψ))
53, 4syl 15 1 ((φψ) → (φψ))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 177 This theorem is referenced by:  biimpi  186  bicom1  190  biimpd  198  ibd  234  pm5.74  235  bi3ant  280  pm5.501  330  bija  344  albi  1564  exbi  1581  cbv2h  1980  sbied  2036  eumo0  2228  2eu6  2289  ceqsalt  2881  vtoclgft  2905  spcgft  2931  pm13.183  2979  reu6  3025  reu3  3026  sbciegft  3076  fv3  5341
 Copyright terms: Public domain W3C validator