Theorem biimp 215

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 207	. . 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 206

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 207

This theorem is referenced by:  biimpi  216  bicom1  221  biimpd  229  ibd  269  pm5.74  270  pm5.501  366  bija  380  albi  1818  spsbbi  2074  cbv2w  2335  cbv2  2401  cbv2h  2404  dfmoeu  2529  2eu6  2650  ax9ALT  2724  ralbi  3085  rexbi  3086  ceqsalt  3481  spcgft  3515  vtoclgft  3518  elabgtOLD  3639  elabgtOLDOLD  3640  reu6  3697  reu3  3698  sbciegftOLD  3791  axpr  5382  axprlem4OLD  5384  fv3  6876  expeq0  14057  t1t0  23235  kqfvima  23617  ufileu  23806  axsepg2ALT  35073  cvmlift2lem1  35289  btwndiff  36015  nn0prpw  36311  bj-animbi  36547  bj-dfbi6  36563  bj-bi3ant  36577  bj-cbv2hv  36785  bj-moeub  36837  bj-ceqsalt0  36872  bj-ceqsalt1  36873  eqab2  38237  sticksstones3  42136  eu6w  42664  or3or  44012  bi33imp12  44481  bi23imp1  44485  bi123imp0  44486  eqsbc2VD  44829  imbi12VD  44862  2uasbanhVD  44900  ssclaxsep  44972  nimnbi  45157  thincciso  49442