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  2367  cbv2  2433  cbv2h  2436  dfmoeu  2561  2eu6  2682  ax9ALT  2756  ralbi  3118  rexbi  3119  ceqsalt  3484  spcgft  3513  vtoclgft  3516  elabgtOLD  3627  reu6  3684  reu3  3685  vn0  4291  axpr  5389  fv3  6904  elirrv  9592  elirrvOLD  9593  expeq0  14236  t1t0  23667  kqfvima  24050  ufileu  24239  r1omhfb  35739  r1omhfbregs  35806  axsepg3ALT  35811  cvmlift2lem1  36068  btwndiff  36793  nn0prpw  37112  bj-bisimpl  37423  bj-bisimpr  37424  bj-animbi  37429  bj-dfbi6  37446  bj-bi3ant  37460  bj-cbv2hv  37710  bj-moeub  37762  bj-ceqsalt0  37797  bj-ceqsalt1  37798  wl-dfcleq  38439  eqab2  39184  sticksstones3  43200  eu6w  43689  or3or  45024  bi33imp12  45475  bi23imp1  45479  bi123imp0  45480  eqsbc2VD  45823  imbi12VD  45856  2uasbanhVD  45894  ssclaxsep  45973  nimnbi  46179  thincciso  50562