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  3070  spc2gv  3557  spc3gv  3561  frpoind  6294  soisoi  7269  isomin  7278  riotaclb  7351  extmptsuppeq  8128  mpoxopynvov0g  8154  fsetcdmex  8797  boxcutc  8875  sdomel  9048  onsdominel  9050  preleqALT  9532  frind  9665  cflim2  10176  cfslbn  10180  cofsmo  10182  fincssdom  10236  fin23lem25  10237  fin23lem26  10238  fin1a2s  10327  pwfseqlem4  10575  ltapr  10958  suplem2pr  10966  qsqueeze  13121  ssfzoulel  13681  ssnn0fi  13910  hashbnd  14261  hashclb  14283  hashgt0elex  14326  hashgt12el  14347  hashgt12el2  14348  2mulprm  16622  pc2dvds  16809  infpnlem1  16840  mndpsuppss  18657  odcl2  19462  ufilmax  23810  ufileu  23822  filufint  23823  hausflim  23884  flimfnfcls  23931  alexsubALTlem3  23952  alexsubALTlem4  23953  reconnlem2  24732  lebnumlem3  24878  rrxmvallem  25320  itg1ge0a  25628  itg2seq  25659  m1lgs  27315  nosepon  27593  sleadd1im  27917  sleadd1  27919  onscutlt  28188  onnolt  28190  lmieu  28747  axlowdimlem14  28918  usgredg2v  29190  cusgrfilem3  29421  cusgrfi  29422  vtxdgoddnumeven  29517  clwwlknon1sn  30062  ex-natded5.13-2  30378  diffib  32483  ordtconnlem1  33890  eulerpartlemgh  34345  bnj23  34684  nn0prpw  36296  meran1  36384  finxpreclem6  37369  wl-spae  37494  poimirlem32  37631  heiborlem1  37790  riotaclbgBAD  38932  primrootspoweq0  42079  aks6d1c2p2  42092  hashscontpow  42095  aks6d1c5lem1  42109  aks6d1c6lem3  42145  ioin9i8  42180  onsupmaxb  43212  onsupsucismax  43252  tfsconcat0b  43319  relpmin  44926  reclt0  45371  limclr  45637  eu2ndop1stv  47110  requad01  47606  line2ylem  48737  line2xlem  48739