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  366  bija  381  albi  1822  spsbbi  2077  cbv2w  2336  cbv2  2403  cbv2h  2406  dfmoeu  2536  2eu6  2658  ax9ALT  2733  ralbi  3092  rexbi  3169  ceqsalt  3452  vtoclgft  3482  spcgft  3517  pm13.183  3590  elabgt  3596  reu6  3656  reu3  3657  sbciegft  3749  axprlem4  5344  fv3  6774  expeq0  13741  t1t0  22407  kqfvima  22789  ufileu  22978  cvmlift2lem1  33164  btwndiff  34256  nn0prpw  34439  bj-animbi  34666  bj-dfbi6  34683  bj-bi3ant  34698  bj-cbv2hv  34906  bj-moeub  34960  bj-ceqsalt0  34996  bj-ceqsalt1  34997  sticksstones3  40032  or3or  41520  bi33imp12  41999  bi23imp1  42004  bi123imp0  42005  eqsbc2VD  42349  imbi12VD  42382  2uasbanhVD  42420  thincciso  46218