Theorem biimp 215

Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.)

Assertion

Ref	Expression
biimp	⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓))

Proof of Theorem biimp

Step	Hyp	Ref	Expression
1		df-bi 207	. . 3 ⊢ ¬ (((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓)))
2		simplim 167	. . 3 ⊢ (¬ (((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓))) → ((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))))
3	1, 2	ax-mp 5	. 2 ⊢ ((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))
4		simplim 167	. 2 ⊢ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 → 𝜓))
5	3, 4	syl 17	1 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  biimpi  216  bicom1  221  biimpd  229  ibd  269  pm5.74  270  pm5.501  366  bija  380  albi  1818  spsbbi  2073  cbv2w  2339  cbv2  2408  cbv2h  2411  dfmoeu  2536  2eu6  2657  ax9ALT  2732  ralbi  3103  rexbi  3104  ceqsalt  3515  spcgft  3549  vtoclgft  3552  elabgt  3672  elabgtOLD  3673  reu6  3732  reu3  3733  sbciegftOLD  3826  axpr  5427  axprlem4OLD  5429  fv3  6924  expeq0  14133  t1t0  23356  kqfvima  23738  ufileu  23927  axsepg2ALT  35097  cvmlift2lem1  35307  btwndiff  36028  nn0prpw  36324  bj-animbi  36560  bj-dfbi6  36576  bj-bi3ant  36590  bj-cbv2hv  36798  bj-moeub  36850  bj-ceqsalt0  36885  bj-ceqsalt1  36886  sticksstones3  42149  eu6w  42686  or3or  44036  bi33imp12  44511  bi23imp1  44515  bi123imp0  44516  eqsbc2VD  44860  imbi12VD  44893  2uasbanhVD  44931  ssclaxsep  44999  nimnbi  45168  thincciso  49102