Theorem biimp 215

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 207	. . 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 206

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 207

This theorem is referenced by:  biimpi  216  bicom1  221  biimpd  229  ibd  269  pm5.74  270  pm5.501  366  bija  380  albi  1819  spsbbi  2076  cbv2w  2337  cbv2  2403  cbv2h  2406  dfmoeu  2531  2eu6  2652  ax9ALT  2726  ralbi  3087  rexbi  3088  ceqsalt  3470  spcgft  3504  vtoclgft  3507  elabgtOLD  3628  elabgtOLDOLD  3629  reu6  3685  reu3  3686  sbciegftOLD  3779  axpr  5365  axprlem4OLD  5367  fv3  6840  elirrv  9483  expeq0  13999  t1t0  23264  kqfvima  23646  ufileu  23835  axsepg2ALT  35093  r1omhfb  35121  r1omhfbregs  35131  cvmlift2lem1  35344  btwndiff  36067  nn0prpw  36363  bj-animbi  36599  bj-dfbi6  36615  bj-bi3ant  36629  bj-cbv2hv  36837  bj-moeub  36889  bj-ceqsalt0  36924  bj-ceqsalt1  36925  eqab2  38289  sticksstones3  42187  eu6w  42715  or3or  44062  bi33imp12  44530  bi23imp1  44534  bi123imp0  44535  eqsbc2VD  44878  imbi12VD  44911  2uasbanhVD  44949  ssclaxsep  45021  nimnbi  45206  thincciso  49491