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  1833  rexim  3073  spc2gv  3555  spc3gv  3559  frpoind  6289  soisoi  7262  isomin  7271  riotaclb  7344  extmptsuppeq  8118  mpoxopynvov0g  8144  fsetcdmex  8787  boxcutc  8865  sdomel  9037  onsdominel  9039  preleqALT  9507  frind  9640  cflim2  10151  cfslbn  10155  cofsmo  10157  fincssdom  10211  fin23lem25  10212  fin23lem26  10213  fin1a2s  10302  pwfseqlem4  10550  ltapr  10933  suplem2pr  10941  qsqueeze  13097  ssfzoulel  13657  ssnn0fi  13889  hashbnd  14240  hashclb  14262  hashgt0elex  14305  hashgt12el  14326  hashgt12el2  14327  2mulprm  16601  pc2dvds  16788  infpnlem1  16819  mndpsuppss  18670  odcl2  19475  ufilmax  23820  ufileu  23832  filufint  23833  hausflim  23894  flimfnfcls  23941  alexsubALTlem3  23962  alexsubALTlem4  23963  reconnlem2  24741  lebnumlem3  24887  rrxmvallem  25329  itg1ge0a  25637  itg2seq  25668  m1lgs  27324  nosepon  27602  sleadd1im  27928  sleadd1  27930  onscutlt  28199  onnolt  28201  lmieu  28760  axlowdimlem14  28931  usgredg2v  29203  cusgrfilem3  29434  cusgrfi  29435  vtxdgoddnumeven  29530  clwwlknon1sn  30075  ex-natded5.13-2  30391  diffib  32496  ordtconnlem1  33932  eulerpartlemgh  34386  bnj23  34725  nn0prpw  36356  meran1  36444  finxpreclem6  37429  wl-spae  37554  poimirlem32  37691  heiborlem1  37850  riotaclbgBAD  38992  primrootspoweq0  42138  aks6d1c2p2  42151  hashscontpow  42154  aks6d1c5lem1  42168  aks6d1c6lem3  42204  ioin9i8  42239  onsupmaxb  43271  onsupsucismax  43311  tfsconcat0b  43378  relpmin  44984  reclt0  45428  limclr  45692  eu2ndop1stv  47155  requad01  47651  line2ylem  48782  line2xlem  48784