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  1819  spsbbi  2078  cbv2w  2339  cbv2  2405  cbv2h  2408  dfmoeu  2533  2eu6  2654  ax9ALT  2728  ralbi  3088  rexbi  3089  ceqsalt  3471  spcgft  3503  vtoclgft  3506  elabgtOLD  3624  elabgtOLDOLD  3625  reu6  3681  reu3  3682  sbciegftOLD  3775  axpr  5369  axprlem4OLD  5371  fv3  6848  elirrv  9492  expeq0  14003  t1t0  23266  kqfvima  23648  ufileu  23837  axsepg2ALT  35118  r1omhfb  35146  r1omhfbregs  35156  cvmlift2lem1  35369  btwndiff  36094  nn0prpw  36390  bj-animbi  36626  bj-dfbi6  36642  bj-bi3ant  36656  bj-cbv2hv  36864  bj-moeub  36916  bj-ceqsalt0  36951  bj-ceqsalt1  36952  eqab2  38308  sticksstones3  42264  eu6w  42797  or3or  44143  bi33imp12  44611  bi23imp1  44615  bi123imp0  44616  eqsbc2VD  44959  imbi12VD  44992  2uasbanhVD  45030  ssclaxsep  45102  nimnbi  45287  thincciso  49581