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  1810  spsbbi  2069  cbv2w  2348  cbv2  2414  cbv2h  2417  dfmoeu  2611  2eu6  2737  ax9ALT  2814  ralbi  3164  ceqsalt  3525  vtoclgft  3551  vtoclgftOLD  3552  spcgft  3584  pm13.183  3656  pm13.183OLD  3657  reu6  3714  reu3  3715  sbciegft  3805  axprlem4  5317  fv3  6681  expeq0  13447  t1t0  21884  kqfvima  22266  ufileu  22455  cvmlift2lem1  32446  btwndiff  33385  nn0prpw  33568  bj-animbi  33791  bj-dfbi6  33805  bj-bi3ant  33820  bj-cbv2hv  34016  bj-moeub  34070  bj-ceqsalt0  34097  bj-ceqsalt1  34098  bj-ax9  34113  or3or  40249  bi33imp12  40701  bi23imp1  40706  bi123imp0  40707  eqsbc3rVD  41051  imbi12VD  41084  2uasbanhVD  41122
  Copyright terms: Public domain W3C validator