Theorem con4d 115

Description: Deduction associated with con4 113. (Contributed by NM, 26-Mar-1995.)

Hypothesis

Ref	Expression
con4d.1	⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒))

Assertion

Ref	Expression
con4d	⊢ (𝜑 → (𝜒 → 𝜓))

Proof of Theorem con4d

Step	Hyp	Ref	Expression
1		con4d.1	. 2 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒))
2		con4 113	. 2 ⊢ ((¬ 𝜓 → ¬ 𝜒) → (𝜒 → 𝜓))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝜒 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by:  mt4d  117  pm2.21d  121  pm2.18OLD  129  con2d  136  con1d  147  impcon4bid  230  con4bid  320  norassOLD  1540  aleximi  1839  spc2gv  3505  spc3gv  3509  frpoind  6174  wfi  6181  soisoi  7115  isomin  7124  riotaclb  7190  extmptsuppeq  7908  mpoxopynvov0g  7934  fsetcdmex  8522  boxcutc  8600  sdomel  8771  onsdominel  8773  preleqALT  9210  cflim2  9842  cfslbn  9846  cofsmo  9848  fincssdom  9902  fin23lem25  9903  fin23lem26  9904  fin1a2s  9993  pwfseqlem4  10241  ltapr  10624  suplem2pr  10632  qsqueeze  12756  ssfzoulel  13301  ssnn0fi  13523  hashbnd  13867  hashclb  13890  hashgt0elex  13933  hashgt12el  13954  hashgt12el2  13955  2mulprm  16213  pc2dvds  16395  infpnlem1  16426  odcl2  18910  ufilmax  22758  ufileu  22770  filufint  22771  hausflim  22832  flimfnfcls  22879  alexsubALTlem3  22900  alexsubALTlem4  22901  reconnlem2  23678  lebnumlem3  23814  rrxmvallem  24255  itg1ge0a  24563  itg2seq  24594  m1lgs  26223  lmieu  26829  axlowdimlem14  27000  usgredg2v  27269  cusgrfilem3  27499  cusgrfi  27500  vtxdgoddnumeven  27595  clwwlknon1sn  28137  ex-natded5.13-2  28453  diffib  30542  ordtconnlem1  31542  eulerpartlemgh  32011  bnj23  32363  frind  33460  nosepon  33554  nn0prpw  34198  meran1  34286  finxpreclem6  35253  wl-spae  35366  poimirlem32  35495  heiborlem1  35655  riotaclbgBAD  36654  ioin9i8  39836  reclt0  42545  limclr  42814  eu2ndop1stv  44232  requad01  44689  mndpsuppss  45323  line2ylem  45713  line2xlem  45715