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  con2d  134  con1d  145  impcon4bid  227  con4bid  317  aleximi  1832  rexim  3077  spc2gv  3579  spc3gv  3583  frpoind  6331  wfiOLD  6340  soisoi  7320  isomin  7329  riotaclb  7401  extmptsuppeq  8185  mpoxopynvov0g  8211  fsetcdmex  8875  boxcutc  8953  sdomel  9136  onsdominel  9138  preleqALT  9629  frind  9762  cflim2  10275  cfslbn  10279  cofsmo  10281  fincssdom  10335  fin23lem25  10336  fin23lem26  10337  fin1a2s  10426  pwfseqlem4  10674  ltapr  11057  suplem2pr  11065  qsqueeze  13215  ssfzoulel  13774  ssnn0fi  14001  hashbnd  14352  hashclb  14374  hashgt0elex  14417  hashgt12el  14438  hashgt12el2  14439  2mulprm  16710  pc2dvds  16897  infpnlem1  16928  mndpsuppss  18741  odcl2  19544  ufilmax  23843  ufileu  23855  filufint  23856  hausflim  23917  flimfnfcls  23964  alexsubALTlem3  23985  alexsubALTlem4  23986  reconnlem2  24765  lebnumlem3  24911  rrxmvallem  25354  itg1ge0a  25662  itg2seq  25693  m1lgs  27349  nosepon  27627  sleadd1im  27937  sleadd1  27939  lmieu  28709  axlowdimlem14  28880  usgredg2v  29152  cusgrfilem3  29383  cusgrfi  29384  vtxdgoddnumeven  29479  clwwlknon1sn  30027  ex-natded5.13-2  30343  diffib  32448  ordtconnlem1  33901  eulerpartlemgh  34356  bnj23  34695  nn0prpw  36287  meran1  36375  finxpreclem6  37360  wl-spae  37485  poimirlem32  37622  heiborlem1  37781  riotaclbgBAD  38918  primrootspoweq0  42065  aks6d1c2p2  42078  hashscontpow  42081  aks6d1c5lem1  42095  aks6d1c6lem3  42131  ioin9i8  42204  onsupmaxb  43210  onsupsucismax  43250  tfsconcat0b  43317  relpmin  44925  reclt0  45366  limclr  45632  eu2ndop1stv  47102  requad01  47583  line2ylem  48679  line2xlem  48681