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  6901  elirrv  9584  elirrvOLD  9585  expeq0  14228  t1t0  23659  kqfvima  24042  ufileu  24231  r1omhfb  35727  r1omhfbregs  35788  axsepg3ALT  35793  cvmlift2lem1  36046  btwndiff  36772  nn0prpw  37091  bj-bisimpl  37402  bj-bisimpr  37403  bj-animbi  37408  bj-dfbi6  37425  bj-bi3ant  37439  bj-cbv2hv  37689  bj-moeub  37741  bj-ceqsalt0  37776  bj-ceqsalt1  37777  wl-dfcleq  38417  eqab2  39162  sticksstones3  43178  eu6w  43667  or3or  45008  bi33imp12  45459  bi23imp1  45463  bi123imp0  45464  eqsbc2VD  45807  imbi12VD  45840  2uasbanhVD  45878  ssclaxsep  45950  nimnbi  46147  thincciso  50530