Theorem biimp 217

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 209	. . 3 ⊢ ¬ (((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓)))
2		simplim 167	. . 3 ⊢ (¬ (((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓))) → ((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))))
3	1, 2	ax-mp 5	. 2 ⊢ ((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))
4		simplim 167	. 2 ⊢ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 → 𝜓))
5	3, 4	syl 17	1 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓))

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

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 209

This theorem is referenced by:  biimpi  218  bicom1  223  biimpd  231  ibd  271  pm5.74  272  pm5.501  368  bija  382  abab  837  albi  1837  spsbbi  2105  cbv2w  2367  cbv2  2433  cbv2h  2436  dfmoeu  2561  2eu6  2682  ax9ALT  2756  ralbi  3116  rexbi  3117  ceqsalt  3486  spcgft  3516  vtoclgft  3519  elabgtOLD  3631  reu6  3687  reu3  3688  axpr  5381  axprlem4OLD  5384  fv3  6880  elirrv  9539  elirrvOLD  9540  expeq0  14099  t1t0  23396  kqfvima  23778  ufileu  23967  r1omhfb  35369  r1omhfbregs  35394  axsepg3ALT  35399  cvmlift2lem1  35613  btwndiff  36338  nn0prpw  36644  bj-bisimpl  36956  bj-bisimpr  36957  bj-animbi  36962  bj-dfbi6  36979  bj-bi3ant  36993  bj-cbv2hv  37243  bj-moeub  37295  bj-ceqsalt0  37330  bj-ceqsalt1  37331  wl-dfcleq  37969  eqab2  38710  sticksstones3  42726  eu6w  43219  or3or  44560  bi33imp12  45028  bi23imp1  45032  bi123imp0  45033  eqsbc2VD  45376  imbi12VD  45409  2uasbanhVD  45447  ssclaxsep  45519  nimnbi  45702  thincciso  50035