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

Theorem biimp 216
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 208 . . 3 ¬ (((𝜑𝜓) → ¬ ((𝜑𝜓) → ¬ (𝜓𝜑))) → ¬ (¬ ((𝜑𝜓) → ¬ (𝜓𝜑)) → (𝜑𝜓)))
2 simplim 168 . . 3 (¬ (((𝜑𝜓) → ¬ ((𝜑𝜓) → ¬ (𝜓𝜑))) → ¬ (¬ ((𝜑𝜓) → ¬ (𝜓𝜑)) → (𝜑𝜓))) → ((𝜑𝜓) → ¬ ((𝜑𝜓) → ¬ (𝜓𝜑))))
31, 2ax-mp 5 . 2 ((𝜑𝜓) → ¬ ((𝜑𝜓) → ¬ (𝜓𝜑)))
4 simplim 168 . 2 (¬ ((𝜑𝜓) → ¬ (𝜓𝜑)) → (𝜑𝜓))
53, 4syl 17 1 ((𝜑𝜓) → (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207
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 208
This theorem is referenced by:  biimpi  217  bicom1  222  biimpd  230  ibd  270  pm5.74  271  pm5.501  368  bija  382  albi  1800  spsbbi  2051  cbv2  2379  cbv2h  2382  dfmoeu  2572  2eu6  2714  ax9ALT  2791  ralbi  3134  ceqsalt  3470  vtoclgft  3496  vtoclgftOLD  3497  spcgft  3530  pm13.183  3597  pm13.183OLD  3598  reu6  3651  reu3  3652  sbciegft  3737  axprlem4  5218  fv3  6556  expeq0  13309  t1t0  21640  kqfvima  22022  ufileu  22211  cvmlift2lem1  32158  btwndiff  33098  nn0prpw  33281  bj-animbi  33503  bj-dfbi6  33517  bj-bi3ant  33532  bj-cbv2hv  33668  bj-moeub  33747  bj-ceqsalt0  33776  bj-ceqsalt1  33777  bj-ax9  33791  or3or  39875  bi33imp12  40382  bi23imp1  40387  bi123imp0  40388  eqsbc3rVD  40732  imbi12VD  40765  2uasbanhVD  40803
  Copyright terms: Public domain W3C validator