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  226  con4bid  316  aleximi  1834  rexim  3086  spc2gv  3584  spc3gv  3588  frpoind  6329  wfiOLD  6338  soisoi  7306  isomin  7315  riotaclb  7388  extmptsuppeq  8152  mpoxopynvov0g  8178  fsetcdmex  8837  boxcutc  8915  sdomel  9104  onsdominel  9106  preleqALT  9591  frind  9724  cflim2  10237  cfslbn  10241  cofsmo  10243  fincssdom  10297  fin23lem25  10298  fin23lem26  10299  fin1a2s  10388  pwfseqlem4  10636  ltapr  11019  suplem2pr  11027  qsqueeze  13159  ssfzoulel  13705  ssnn0fi  13929  hashbnd  14275  hashclb  14297  hashgt0elex  14340  hashgt12el  14361  hashgt12el2  14362  2mulprm  16609  pc2dvds  16791  infpnlem1  16822  odcl2  19394  ufilmax  23335  ufileu  23347  filufint  23348  hausflim  23409  flimfnfcls  23456  alexsubALTlem3  23477  alexsubALTlem4  23478  reconnlem2  24267  lebnumlem3  24403  rrxmvallem  24845  itg1ge0a  25153  itg2seq  25184  m1lgs  26813  nosepon  27090  sleadd1im  27381  sleadd1  27383  lmieu  27895  axlowdimlem14  28073  usgredg2v  28344  cusgrfilem3  28574  cusgrfi  28575  vtxdgoddnumeven  28670  clwwlknon1sn  29213  ex-natded5.13-2  29529  diffib  31618  ordtconnlem1  32719  eulerpartlemgh  33192  bnj23  33544  nn0prpw  34996  meran1  35084  finxpreclem6  36065  wl-spae  36178  poimirlem32  36308  heiborlem1  36468  riotaclbgBAD  37613  aks6d1c2p2  40746  ioin9i8  40822  onsupmaxb  41745  onsupsucismax  41786  tfsconcat0b  41853  reclt0  43860  limclr  44130  eu2ndop1stv  45591  requad01  46047  mndpsuppss  46681  line2ylem  47071  line2xlem  47073