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

Theorem biimp 204
 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 196 . . 3 ¬ (((𝜑𝜓) → ¬ ((𝜑𝜓) → ¬ (𝜓𝜑))) → ¬ (¬ ((𝜑𝜓) → ¬ (𝜓𝜑)) → (𝜑𝜓)))
2 simplim 162 . . 3 (¬ (((𝜑𝜓) → ¬ ((𝜑𝜓) → ¬ (𝜓𝜑))) → ¬ (¬ ((𝜑𝜓) → ¬ (𝜓𝜑)) → (𝜑𝜓))) → ((𝜑𝜓) → ¬ ((𝜑𝜓) → ¬ (𝜓𝜑))))
31, 2ax-mp 5 . 2 ((𝜑𝜓) → ¬ ((𝜑𝜓) → ¬ (𝜓𝜑)))
4 simplim 162 . 2 (¬ ((𝜑𝜓) → ¬ (𝜓𝜑)) → (𝜑𝜓))
53, 4syl 17 1 ((𝜑𝜓) → (𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195 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 196 This theorem is referenced by:  biimpi  205  bicom1  210  biimpd  218  ibd  257  pm5.74  258  pm5.501  355  bija  369  albi  1736  exbiOLD  1763  cbv2h  2257  mo2v  2465  2eu6  2546  eleq2dOLD  2674  ceqsalt  3201  vtoclgft  3227  vtoclgftOLD  3228  spcgft  3258  pm13.183  3313  reu6  3362  reu3  3363  sbciegft  3433  fv3  6116  expeq0  12752  t1t0  20962  kqfvima  21343  ufileu  21533  cvmlift2lem1  30538  btwndiff  31304  nn0prpw  31488  bj-dfbi6  31730  bj-bi3ant  31747  bj-ssbbi  31811  bj-cbv2hv  31918  bj-eumo0  32018  bj-ceqsalt0  32067  bj-ceqsalt1  32068  bj-ax9  32083  or3or  37339  bi33imp12  37717  bi23imp1  37722  bi123imp0  37723  eqsbc3rVD  38097  imbi12VD  38131  2uasbanhVD  38169
 Copyright terms: Public domain W3C validator