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  228  con4bid  318  aleximi  1839  rexim  3081  spc2gv  3545  spc3gv  3549  frpoind  6300  soisoi  7279  isomin  7288  riotaclb  7361  extmptsuppeq  8135  mpoxopynvov0g  8161  fsetcdmex  8807  boxcutc  8886  sdomel  9059  onsdominel  9061  preleqALT  9536  frind  9672  cflim2  10183  cfslbn  10187  cofsmo  10189  fincssdom  10243  fin23lem25  10244  fin23lem26  10245  fin1a2s  10334  pwfseqlem4  10583  ltapr  10966  suplem2pr  10974  qsqueeze  13151  ssfzoulel  13713  ssnn0fi  13945  hashbnd  14296  hashclb  14318  hashgt0elex  14361  hashgt12el  14382  hashgt12el2  14383  2mulprm  16660  pc2dvds  16848  infpnlem1  16879  mndpsuppss  18731  odcl2  19538  ufilmax  23897  ufileu  23909  filufint  23910  hausflim  23971  flimfnfcls  24018  alexsubALTlem3  24039  alexsubALTlem4  24040  reconnlem2  24818  lebnumlem3  24955  rrxmvallem  25396  itg1ge0a  25703  itg2seq  25734  m1lgs  27376  nosepon  27654  leadds1im  28004  leadds1  28006  oncutlt  28281  onnolt  28283  bdaypw2n0bndlem  28480  lmieu  28877  axlowdimlem14  29049  usgredg2v  29321  cusgrfilem3  29551  cusgrfi  29552  vtxdgoddnumeven  29647  clwwlknon1sn  30195  ex-natded5.13-2  30511  diffib  32616  ordtconnlem1  34115  eulerpartlemgh  34569  bnj23  34908  nn0prpw  36558  meran1  36646  mh-regprimbi  36780  finxpreclem6  37765  wl-spae  37899  poimirlem32  38026  heiborlem1  38185  riotaclbgBAD  39453  primrootspoweq0  42598  aks6d1c2p2  42611  hashscontpow  42614  aks6d1c5lem1  42628  aks6d1c6lem3  42664  ioin9i8  42699  onsupmaxb  43691  onsupsucismax  43731  tfsconcat0b  43798  relpmin  45403  reclt0  45842  limclr  46105  eu2ndop1stv  47595  requad01  48119  line2ylem  49249  line2xlem  49251