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

Theorem biimp 214
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 206 . . 3 ¬ (((𝜑𝜓) → ¬ ((𝜑𝜓) → ¬ (𝜓𝜑))) → ¬ (¬ ((𝜑𝜓) → ¬ (𝜓𝜑)) → (𝜑𝜓)))
2 simplim 167 . . 3 (¬ (((𝜑𝜓) → ¬ ((𝜑𝜓) → ¬ (𝜓𝜑))) → ¬ (¬ ((𝜑𝜓) → ¬ (𝜓𝜑)) → (𝜑𝜓))) → ((𝜑𝜓) → ¬ ((𝜑𝜓) → ¬ (𝜓𝜑))))
31, 2ax-mp 5 . 2 ((𝜑𝜓) → ¬ ((𝜑𝜓) → ¬ (𝜓𝜑)))
4 simplim 167 . 2 (¬ ((𝜑𝜓) → ¬ (𝜓𝜑)) → (𝜑𝜓))
53, 4syl 17 1 ((𝜑𝜓) → (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205
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 206
This theorem is referenced by:  biimpi  215  bicom1  220  biimpd  228  ibd  269  pm5.74  270  pm5.501  367  bija  382  albi  1821  spsbbi  2077  cbv2w  2334  cbv2  2402  cbv2h  2405  dfmoeu  2531  2eu6  2653  ax9ALT  2728  ralbi  3103  rexbi  3104  ceqsalt  3474  vtoclgft  3508  spcgft  3546  pm13.183  3619  elabgt  3625  reu6  3685  reu3  3686  sbciegft  3778  axprlem4  5382  fv3  6861  expeq0  14004  t1t0  22715  kqfvima  23097  ufileu  23286  cvmlift2lem1  33953  btwndiff  34658  nn0prpw  34841  bj-animbi  35068  bj-dfbi6  35085  bj-bi3ant  35100  bj-cbv2hv  35308  bj-moeub  35361  bj-ceqsalt0  35397  bj-ceqsalt1  35398  sticksstones3  40602  or3or  42383  bi33imp12  42860  bi23imp1  42865  bi123imp0  42866  eqsbc2VD  43210  imbi12VD  43243  2uasbanhVD  43281  nimnbi  43467  thincciso  47155
  Copyright terms: Public domain W3C validator