Theorem biimp 216

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 208	. . 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 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  367  bija  381  albi  1825  spsbbi  2084  cbv2w  2345  cbv2  2411  cbv2h  2414  dfmoeu  2539  2eu6  2660  ax9ALT  2734  ralbi  3094  rexbi  3095  ceqsalt  3464  spcgft  3495  vtoclgft  3498  elabgtOLD  3611  reu6  3667  reu3  3668  axpr  5356  axprlem4OLD  5359  fv3  6845  elirrv  9502  elirrvOLD  9503  expeq0  14045  t1t0  23331  kqfvima  23713  ufileu  23902  r1omhfb  35293  r1omhfbregs  35318  axsepg3ALT  35323  cvmlift2lem1  35530  btwndiff  36255  nn0prpw  36551  bj-bisimpl  36863  bj-bisimpr  36864  bj-animbi  36869  bj-dfbi6  36886  bj-bi3ant  36900  bj-cbv2hv  37150  bj-moeub  37202  bj-ceqsalt0  37237  bj-ceqsalt1  37238  wl-dfcleq  37876  eqab2  38617  sticksstones3  42633  eu6w  43126  or3or  44467  bi33imp12  44935  bi23imp1  44939  bi123imp0  44940  eqsbc2VD  45283  imbi12VD  45316  2uasbanhVD  45354  ssclaxsep  45426  nimnbi  45610  thincciso  49943