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  1845  spsbbi  2113  cbv2w  2375  cbv2  2441  cbv2h  2444  dfmoeu  2569  2eu6  2690  ax9ALT  2764  ralbi  3126  rexbi  3127  ceqsalt  3496  spcgft  3526  vtoclgft  3529  elabgtOLD  3641  reu6  3698  reu3  3699  axpr  5396  axprlem4OLD  5399  fv3  6897  elirrv  9555  elirrvOLD  9556  expeq0  14124  t1t0  23470  kqfvima  23852  ufileu  24041  r1omhfb  35444  r1omhfbregs  35469  axsepg3ALT  35474  cvmlift2lem1  35689  btwndiff  36414  nn0prpw  36719  bj-bisimpl  37030  bj-bisimpr  37031  bj-animbi  37036  bj-dfbi6  37053  bj-bi3ant  37067  bj-cbv2hv  37317  bj-moeub  37369  bj-ceqsalt0  37404  bj-ceqsalt1  37405  wl-dfcleq  38043  eqab2  38784  sticksstones3  42800  eu6w  43293  or3or  44634  bi33imp12  45085  bi23imp1  45089  bi123imp0  45090  eqsbc2VD  45433  imbi12VD  45466  2uasbanhVD  45504  ssclaxsep  45576  nimnbi  45766  thincciso  50109