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  1850  spsbbi  2109  cbv2w  2366  cbv2  2432  cbv2h  2435  dfmoeu  2560  2eu6  2681  ax9ALT  2755  ralbi  3117  rexbi  3118  ceqsalt  3483  spcgft  3512  vtoclgft  3515  elabgtOLD  3626  reu6  3683  reu3  3684  vn0  4290  axpr  5388  fv3  6904  elirrv  9595  elirrvOLD  9596  expeq0  14239  t1t0  23672  kqfvima  24055  ufileu  24244  reu6f  35756  rmo6  35757  r1omhfb  35791  r1omhfbregs  35862  axsepg3ALT  35867  cvmlift2lem1  36154  btwndiff  36885  nn0prpw  37204  bj-bisimpl  37515  bj-bisimpr  37516  bj-animbi  37521  bj-dfbi6  37538  bj-bi3ant  37552  bj-cbv2hv  37802  bj-moeub  37854  bj-ceqsalt0  37889  bj-ceqsalt1  37890  wl-dfcleq  38531  eqab2  39276  sticksstones3  43292  eu6w  43781  or3or  45117  bi33imp12  45568  bi23imp1  45572  bi123imp0  45573  eqsbc2VD  45916  imbi12VD  45949  2uasbanhVD  45987  ssclaxsep  46066  nimnbi  46272  thincciso  50682