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  365  bija  379  albi  1812  spsbbi  2068  cbv2w  2327  cbv2  2396  cbv2h  2399  dfmoeu  2524  2eu6  2645  ax9ALT  2720  ralbi  3092  rexbi  3093  ceqsalt  3494  vtoclgft  3530  spcgft  3572  elabgt  3657  elabgtOLD  3658  reu6  3718  reu3  3719  sbciegftOLD  3812  axprlem4  5426  fv3  6914  expeq0  14093  t1t0  23296  kqfvima  23678  ufileu  23867  cvmlift2lem1  35043  btwndiff  35754  nn0prpw  35938  bj-animbi  36165  bj-dfbi6  36182  bj-bi3ant  36197  bj-cbv2hv  36405  bj-moeub  36457  bj-ceqsalt0  36493  bj-ceqsalt1  36494  sticksstones3  41751  eu6w  42236  or3or  43595  bi33imp12  44071  bi23imp1  44076  bi123imp0  44077  eqsbc2VD  44421  imbi12VD  44454  2uasbanhVD  44492  nimnbi  44674  thincciso  48241