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  1830  rexim  3093  spc2gv  3613  spc3gv  3617  frpoind  6374  wfiOLD  6383  soisoi  7364  isomin  7373  riotaclb  7446  extmptsuppeq  8229  mpoxopynvov0g  8255  fsetcdmex  8921  boxcutc  8999  sdomel  9190  onsdominel  9192  preleqALT  9686  frind  9819  cflim2  10332  cfslbn  10336  cofsmo  10338  fincssdom  10392  fin23lem25  10393  fin23lem26  10394  fin1a2s  10483  pwfseqlem4  10731  ltapr  11114  suplem2pr  11122  qsqueeze  13263  ssfzoulel  13810  ssnn0fi  14036  hashbnd  14385  hashclb  14407  hashgt0elex  14450  hashgt12el  14471  hashgt12el2  14472  2mulprm  16740  pc2dvds  16926  infpnlem1  16957  odcl2  19607  ufilmax  23936  ufileu  23948  filufint  23949  hausflim  24010  flimfnfcls  24057  alexsubALTlem3  24078  alexsubALTlem4  24079  reconnlem2  24868  lebnumlem3  25014  rrxmvallem  25457  itg1ge0a  25766  itg2seq  25797  m1lgs  27450  nosepon  27728  sleadd1im  28038  sleadd1  28040  lmieu  28810  axlowdimlem14  28988  usgredg2v  29262  cusgrfilem3  29493  cusgrfi  29494  vtxdgoddnumeven  29589  clwwlknon1sn  30132  ex-natded5.13-2  30448  diffib  32551  ordtconnlem1  33870  eulerpartlemgh  34343  bnj23  34694  nn0prpw  36289  meran1  36377  finxpreclem6  37362  wl-spae  37475  poimirlem32  37612  heiborlem1  37771  riotaclbgBAD  38910  primrootspoweq0  42063  aks6d1c2p2  42076  hashscontpow  42079  aks6d1c5lem1  42093  aks6d1c6lem3  42129  ioin9i8  42201  onsupmaxb  43200  onsupsucismax  43241  tfsconcat0b  43308  reclt0  45306  limclr  45576  eu2ndop1stv  47040  requad01  47495  mndpsuppss  48096  line2ylem  48485  line2xlem  48487