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  2371  cbv2  2437  cbv2h  2440  dfmoeu  2565  2eu6  2686  ax9ALT  2760  ralbi  3122  rexbi  3123  ceqsalt  3490  spcgft  3519  vtoclgft  3522  elabgtOLD  3634  reu6  3691  reu3  3692  vn0  4298  axpr  5400  axprlem4OLD  5403  fv3  6903  elirrv  9562  elirrvOLD  9563  expeq0  14141  t1t0  23534  kqfvima  23916  ufileu  24105  r1omhfb  35525  r1omhfbregs  35566  axsepg3ALT  35571  cvmlift2lem1  35807  btwndiff  36532  nn0prpw  36867  bj-bisimpl  37178  bj-bisimpr  37179  bj-animbi  37184  bj-dfbi6  37201  bj-bi3ant  37215  bj-cbv2hv  37465  bj-moeub  37517  bj-ceqsalt0  37552  bj-ceqsalt1  37553  wl-dfcleq  38193  eqab2  38932  sticksstones3  42948  eu6w  43441  or3or  44782  bi33imp12  45233  bi23imp1  45237  bi123imp0  45238  eqsbc2VD  45581  imbi12VD  45614  2uasbanhVD  45652  ssclaxsep  45724  nimnbi  45914  thincciso  50264