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  1820  spsbbi  2079  cbv2w  2342  cbv2  2408  cbv2h  2411  dfmoeu  2536  2eu6  2658  ax9ALT  2732  ralbi  3093  rexbi  3094  ceqsalt  3464  spcgft  3495  vtoclgft  3498  elabgtOLD  3616  elabgtOLDOLD  3617  reu6  3673  reu3  3674  sbciegftOLD  3767  axpr  5364  axprlem4OLD  5367  fv3  6852  elirrv  9505  expeq0  14045  t1t0  23323  kqfvima  23705  ufileu  23894  axsepg2ALT  35242  r1omhfb  35272  r1omhfbregs  35297  cvmlift2lem1  35500  btwndiff  36225  nn0prpw  36521  bj-bisimpl  36833  bj-bisimpr  36834  bj-animbi  36839  bj-dfbi6  36856  bj-bi3ant  36870  bj-cbv2hv  37120  bj-moeub  37172  bj-ceqsalt0  37207  bj-ceqsalt1  37208  wl-dfcleq  37844  eqab2  38585  sticksstones3  42601  eu6w  43123  or3or  44468  bi33imp12  44936  bi23imp1  44940  bi123imp0  44941  eqsbc2VD  45284  imbi12VD  45317  2uasbanhVD  45355  ssclaxsep  45427  nimnbi  45611  thincciso  49940