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  228  con4bid  318  norass  1519  aleximi  1813  spc2gv  3543  spc3gv  3547  wfi  6056  soisoi  6944  isomin  6953  riotaclb  7015  extmptsuppeq  7705  mpoxopynvov0g  7731  boxcutc  8353  sdomel  8511  onsdominel  8513  preleqALT  8926  cflim2  9531  cfslbn  9535  cofsmo  9537  fincssdom  9591  fin23lem25  9592  fin23lem26  9593  fin1a2s  9682  pwfseqlem4  9930  ltapr  10313  suplem2pr  10321  qsqueeze  12444  ssfzoulel  12981  ssnn0fi  13203  hashbnd  13546  hashclb  13569  hashgt0elex  13610  hashgt12el  13631  hashgt12el2  13632  2mulprm  15866  pc2dvds  16044  infpnlem1  16075  odcl2  18422  ufilmax  22199  ufileu  22211  filufint  22212  hausflim  22273  flimfnfcls  22320  alexsubALTlem3  22341  alexsubALTlem4  22342  reconnlem2  23118  lebnumlem3  23250  rrxmvallem  23690  itg1ge0a  23995  itg2seq  24026  m1lgs  25646  lmieu  26252  axlowdimlem14  26424  usgredg2v  26692  cusgrfilem3  26922  cusgrfi  26923  vtxdgoddnumeven  27018  clwwlknon1sn  27566  ex-natded5.13-2  27887  ordtconnlem1  30784  eulerpartlemgh  31253  bnj23  31605  frpoind  32689  frind  32694  nosepon  32781  nn0prpw  33280  meran1  33368  finxpreclem6  34208  wl-spae  34294  poimirlem32  34455  heiborlem1  34621  riotaclbgBAD  35621  ioin9i8  38629  reclt0  41204  limclr  41478  eu2ndop1stv  42840  requad01  43268  mndpsuppss  43899  line2ylem  44219  line2xlem  44221