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 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210

This theorem is referenced by:  biimpi  219  bicom1  224  biimpd  232  ibd  272  pm5.74  273  pm5.501  369  bija  383  abab  839  albi  1848  spsbbi  2107  cbv2w  2369  cbv2  2435  cbv2h  2438  dfmoeu  2563  2eu6  2684  ax9ALT  2758  ralbi  3120  rexbi  3121  ceqsalt  3488  spcgft  3518  vtoclgft  3521  elabgtOLD  3633  reu6  3690  reu3  3691  vn0  4299  axpr  5400  axprlem4OLD  5403  fv3  6901  elirrv  9560  elirrvOLD  9561  expeq0  14130  t1t0  23486  kqfvima  23868  ufileu  24057  r1omhfb  35489  r1omhfbregs  35531  axsepg3ALT  35536  cvmlift2lem1  35775  btwndiff  36500  nn0prpw  36815  bj-bisimpl  37126  bj-bisimpr  37127  bj-animbi  37132  bj-dfbi6  37149  bj-bi3ant  37163  bj-cbv2hv  37413  bj-moeub  37465  bj-ceqsalt0  37500  bj-ceqsalt1  37501  wl-dfcleq  38141  eqab2  38880  sticksstones3  42896  eu6w  43391  or3or  44732  bi33imp12  45183  bi23imp1  45187  bi123imp0  45188  eqsbc2VD  45531  imbi12VD  45564  2uasbanhVD  45602  ssclaxsep  45674  nimnbi  45864  thincciso  50214