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

Theorem bi2 189
 Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.) (Proof shortened by Wolf Lammen, 11-Nov-2012.)
Assertion
Ref Expression
bi2 ((φψ) → (ψφ))

Proof of Theorem bi2
StepHypRef Expression
1 dfbi1 184 . 2 ((φψ) ↔ ¬ ((φψ) → ¬ (ψφ)))
2 simprim 142 . 2 (¬ ((φψ) → ¬ (ψφ)) → (ψφ))
31, 2sylbi 187 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:  bicom1  190  pm5.74  235  bi3ant  280  bija  344  pm4.72  846  exbir  1365  simplbi2comg  1373  albi  1564  exbi  1581  cbv2h  1980  sbied  2036  2eu6  2289  ceqsalt  2881  euind  3023  reu6  3025  reuind  3039  sbciegft  3076  iota4  4357  fv3  5341
 Copyright terms: Public domain W3C validator