Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  biimp Structured version   Visualization version   GIF version

Theorem biimp 218
 Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.)
Assertion
Ref Expression
biimp ((𝜑𝜓) → (𝜑𝜓))

Proof of Theorem biimp
StepHypRef Expression
1 df-bi 210 . . 3 ¬ (((𝜑𝜓) → ¬ ((𝜑𝜓) → ¬ (𝜓𝜑))) → ¬ (¬ ((𝜑𝜓) → ¬ (𝜓𝜑)) → (𝜑𝜓)))
2 simplim 170 . . 3 (¬ (((𝜑𝜓) → ¬ ((𝜑𝜓) → ¬ (𝜓𝜑))) → ¬ (¬ ((𝜑𝜓) → ¬ (𝜓𝜑)) → (𝜑𝜓))) → ((𝜑𝜓) → ¬ ((𝜑𝜓) → ¬ (𝜓𝜑))))
31, 2ax-mp 5 . 2 ((𝜑𝜓) → ¬ ((𝜑𝜓) → ¬ (𝜓𝜑)))
4 simplim 170 . 2 (¬ ((𝜑𝜓) → ¬ (𝜓𝜑)) → (𝜑𝜓))
53, 4syl 17 1 ((𝜑𝜓) → (𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209 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 210 This theorem is referenced by:  biimpi  219  bicom1  224  biimpd  232  ibd  272  pm5.74  273  pm5.501  370  bija  385  albi  1820  spsbbi  2078  cbv2w  2346  cbv2  2412  cbv2h  2415  dfmoeu  2594  2eu6  2719  ax9ALT  2794  ralbi  3135  ceqsalt  3475  vtoclgft  3502  vtoclgftOLD  3503  spcgft  3536  pm13.183  3607  reu6  3667  reu3  3668  sbciegft  3758  axprlem4  5296  fv3  6673  expeq0  13475  t1t0  21994  kqfvima  22376  ufileu  22565  cvmlift2lem1  32728  btwndiff  33748  nn0prpw  33931  bj-animbi  34158  bj-dfbi6  34172  bj-bi3ant  34187  bj-cbv2hv  34385  bj-moeub  34439  bj-ceqsalt0  34475  bj-ceqsalt1  34476  bj-ax9  34491  or3or  40895  bi33imp12  41367  bi23imp1  41372  bi123imp0  41373  eqsbc3rVD  41717  imbi12VD  41750  2uasbanhVD  41788
 Copyright terms: Public domain W3C validator