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  2341  cbv2  2407  cbv2h  2410  dfmoeu  2535  2eu6  2657  ax9ALT  2731  ralbi  3092  rexbi  3093  ceqsalt  3463  spcgft  3494  vtoclgft  3497  elabgtOLD  3615  elabgtOLDOLD  3616  reu6  3672  reu3  3673  sbciegftOLD  3766  axpr  5369  axprlem4OLD  5372  fv3  6858  elirrv  9512  expeq0  14054  t1t0  23313  kqfvima  23695  ufileu  23884  axsepg2ALT  35226  r1omhfb  35256  r1omhfbregs  35281  cvmlift2lem1  35484  btwndiff  36209  nn0prpw  36505  bj-bisimpl  36817  bj-bisimpr  36818  bj-animbi  36823  bj-dfbi6  36840  bj-bi3ant  36854  bj-cbv2hv  37104  bj-moeub  37156  bj-ceqsalt0  37191  bj-ceqsalt1  37192  wl-dfcleq  37830  eqab2  38571  sticksstones3  42587  eu6w  43109  or3or  44450  bi33imp12  44918  bi23imp1  44922  bi123imp0  44923  eqsbc2VD  45266  imbi12VD  45299  2uasbanhVD  45337  ssclaxsep  45409  nimnbi  45593  thincciso  49928