Theorem biimp 205

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

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

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 197

This theorem is referenced by:  biimpi  206  bicom1  211  biimpd  219  ibd  258  pm5.74  259  pm5.501  355  bija  369  albi  1786  cbv2h  2305  mo2v  2505  2eu6  2587  ceqsalt  3259  vtoclgft  3285  vtoclgftOLD  3286  spcgft  3316  pm13.183  3376  reu6  3428  reu3  3429  sbciegft  3499  fv3  6244  expeq0  12930  t1t0  21200  kqfvima  21581  ufileu  21770  cvmlift2lem1  31410  btwndiff  32259  nn0prpw  32443  bj-dfbi6  32685  bj-bi3ant  32699  bj-ssbbi  32747  bj-cbv2hv  32856  bj-eumo0  32955  bj-ceqsalt0  32998  bj-ceqsalt1  32999  bj-ax9  33015  bj-ax9-2  33016  or3or  38636  bi33imp12  39013  bi23imp1  39018  bi123imp0  39019  eqsbc3rVD  39389  imbi12VD  39423  2uasbanhVD  39461