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  1820  spsbbi  2076  cbv2w  2333  cbv2  2402  cbv2h  2405  dfmoeu  2530  2eu6  2652  ax9ALT  2727  ralbi  3103  rexbi  3104  raleleq  3337  ceqsalt  3505  vtoclgft  3540  spcgft  3578  pm13.183  3655  elabgt  3661  reu6  3721  reu3  3722  sbciegft  3814  axprlem4  5423  fv3  6906  expeq0  14054  t1t0  22843  kqfvima  23225  ufileu  23414  cvmlift2lem1  34281  btwndiff  34987  nn0prpw  35196  bj-animbi  35423  bj-dfbi6  35440  bj-bi3ant  35455  bj-cbv2hv  35663  bj-moeub  35716  bj-ceqsalt0  35752  bj-ceqsalt1  35753  sticksstones3  40952  or3or  42759  bi33imp12  43236  bi23imp1  43241  bi123imp0  43242  eqsbc2VD  43586  imbi12VD  43619  2uasbanhVD  43657  nimnbi  43843  thincciso  47622