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  2112  cbv2w  2370  cbv2  2435  cbv2h  2438  dfmoeu  2563  2eu6  2684  ax9ALT  2758  ralbi  3121  rexbi  3122  ceqsalt  3487  spcgft  3516  vtoclgft  3519  elabgtOLD  3630  reu6  3687  reu3  3688  vn0  4294  axpr  5396  fv3  6934  elirrv  9628  elirrvOLD  9629  expeq0  14275  t1t0  23721  kqfvima  24104  ufileu  24293  reu6f  35820  rmo6  35821  eqhf  35861  eqhfregs  35946  axsepg3ALT  35951  cvmlift2lem1  36275  btwndiff  37007  nn0prpw  37326  bj-bisimpl  37637  bj-bisimpr  37638  bj-animbi  37643  bj-dfbi6  37660  bj-bi3ant  37674  bj-cbv2hv  37924  bj-moeub  37976  bj-ceqsalt0  38011  bj-ceqsalt1  38012  wl-dfcleq  38705  eqab2  39448  sticksstones3  43464  eu6w  43953  or3or  45284  bi33imp12  45734  bi23imp1  45738  bi123imp0  45739  eqsbc2VD  46082  imbi12VD  46115  2uasbanhVD  46153  ssclaxsep  46236  nimnbi  46451  thincciso  50919