Theorem biimp 218

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 210	. . 3 ⊢ ¬ (((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓)))
2		simplim 168	. . 3 ⊢ (¬ (((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓))) → ((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))))
3	1, 2	ax-mp 5	. 2 ⊢ ((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))
4		simplim 168	. 2 ⊢ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 → 𝜓))
5	3, 4	syl 18	1 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  biimpi  219  bicom1  224  biimpd  232  ibd  272  pm5.74  273  pm5.501  369  bija  383  abab  840  albi  1851  spsbbi  2110  cbv2w  2366  cbv2  2432  cbv2h  2435  dfmoeu  2560  2eu6  2681  ax9ALT  2755  ralbi  3117  rexbi  3118  ceqsalt  3483  spcgft  3512  vtoclgft  3515  elabgtOLD  3627  reu6  3684  reu3  3685  vn0  4291  axpr  5392  axprlem4OLD  5395  fv3  6896  elirrv  9569  elirrvOLD  9570  expeq0  14156  t1t0  23573  kqfvima  23956  ufileu  24145  r1omhfb  35622  r1omhfbregs  35663  axsepg3ALT  35668  cvmlift2lem1  35881  btwndiff  36607  nn0prpw  36942  bj-bisimpl  37253  bj-bisimpr  37254  bj-animbi  37259  bj-dfbi6  37276  bj-bi3ant  37290  bj-cbv2hv  37540  bj-moeub  37592  bj-ceqsalt0  37627  bj-ceqsalt1  37628  wl-dfcleq  38268  eqab2  38998  sticksstones3  43014  eu6w  43522  or3or  44863  bi33imp12  45314  bi23imp1  45318  bi123imp0  45319  eqsbc2VD  45662  imbi12VD  45695  2uasbanhVD  45733  ssclaxsep  45805  nimnbi  45995  thincciso  50379