Theorem biimp 214

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

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 206

This theorem is referenced by:  biimpi  215  bicom1  220  biimpd  228  ibd  268  pm5.74  269  pm5.501  367  bija  382  albi  1821  spsbbi  2076  cbv2w  2334  cbv2  2403  cbv2h  2406  dfmoeu  2536  2eu6  2658  ax9ALT  2733  ralbi  3089  rexbi  3173  ceqsalt  3462  vtoclgft  3492  spcgft  3527  pm13.183  3597  elabgt  3603  reu6  3661  reu3  3662  sbciegft  3754  axprlem4  5349  fv3  6792  expeq0  13813  t1t0  22499  kqfvima  22881  ufileu  23070  cvmlift2lem1  33264  btwndiff  34329  nn0prpw  34512  bj-animbi  34739  bj-dfbi6  34756  bj-bi3ant  34771  bj-cbv2hv  34979  bj-moeub  35033  bj-ceqsalt0  35069  bj-ceqsalt1  35070  sticksstones3  40104  or3or  41631  bi33imp12  42110  bi23imp1  42115  bi123imp0  42116  eqsbc2VD  42460  imbi12VD  42493  2uasbanhVD  42531  thincciso  46330