Theorem biimp 216

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

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

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 208

This theorem is referenced by:  biimpi  217  bicom1  222  biimpd  230  ibd  270  pm5.74  271  pm5.501  368  bija  382  albi  1800  spsbbi  2051  cbv2  2379  cbv2h  2382  dfmoeu  2572  2eu6  2714  ax9ALT  2791  ralbi  3134  ceqsalt  3470  vtoclgft  3496  vtoclgftOLD  3497  spcgft  3530  pm13.183  3597  pm13.183OLD  3598  reu6  3651  reu3  3652  sbciegft  3737  axprlem4  5218  fv3  6556  expeq0  13309  t1t0  21640  kqfvima  22022  ufileu  22211  cvmlift2lem1  32158  btwndiff  33098  nn0prpw  33281  bj-animbi  33503  bj-dfbi6  33517  bj-bi3ant  33532  bj-cbv2hv  33668  bj-moeub  33747  bj-ceqsalt0  33776  bj-ceqsalt1  33777  bj-ax9  33791  or3or  39875  bi33imp12  40382  bi23imp1  40387  bi123imp0  40388  eqsbc3rVD  40732  imbi12VD  40765  2uasbanhVD  40803