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  3084  rexbi  3085  ceqsalt  3472  spcgft  3506  vtoclgft  3509  elabgtOLD  3630  elabgtOLDOLD  3631  reu6  3688  reu3  3689  sbciegftOLD  3782  axpr  5369  axprlem4OLD  5371  fv3  6844  elirrv  9508  expeq0  14017  t1t0  23251  kqfvima  23633  ufileu  23822  axsepg2ALT  35052  cvmlift2lem1  35277  btwndiff  36003  nn0prpw  36299  bj-animbi  36535  bj-dfbi6  36551  bj-bi3ant  36565  bj-cbv2hv  36773  bj-moeub  36825  bj-ceqsalt0  36860  bj-ceqsalt1  36861  eqab2  38225  sticksstones3  42124  eu6w  42652  or3or  43999  bi33imp12  44468  bi23imp1  44472  bi123imp0  44473  eqsbc2VD  44816  imbi12VD  44849  2uasbanhVD  44887  ssclaxsep  44959  nimnbi  45144  thincciso  49442