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 169	. . 3 ⊢ (¬ (((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓))) → ((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))))
3	1, 2	ax-mp 5	. 2 ⊢ ((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))
4		simplim 169	. 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  369  bija  384  albi  1819  spsbbi  2078  cbv2w  2357  cbv2  2423  cbv2h  2426  dfmoeu  2618  2eu6  2742  ax9ALT  2819  ralbi  3169  ceqsalt  3529  vtoclgft  3555  vtoclgftOLD  3556  spcgft  3589  pm13.183  3661  pm13.183OLD  3662  reu6  3719  reu3  3720  sbciegft  3810  axprlem4  5329  fv3  6690  expeq0  13462  t1t0  21958  kqfvima  22340  ufileu  22529  cvmlift2lem1  32551  btwndiff  33490  nn0prpw  33673  bj-animbi  33896  bj-dfbi6  33910  bj-bi3ant  33925  bj-cbv2hv  34121  bj-moeub  34175  bj-ceqsalt0  34202  bj-ceqsalt1  34203  bj-ax9  34218  or3or  40378  bi33imp12  40831  bi23imp1  40836  bi123imp0  40837  eqsbc3rVD  41181  imbi12VD  41214  2uasbanhVD  41252