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  229  con4bid  319  aleximi  1851  rexim  3102  spc2gv  3559  spc3gv  3563  frpoind  6325  soisoi  7308  isomin  7317  riotaclb  7390  extmptsuppeq  8163  mpoxopynvov0g  8189  fsetcdmex  8840  boxcutc  8919  sdomel  9092  onsdominel  9094  preleqALT  9569  frind  9705  cflim2  10217  cfslbn  10221  cofsmo  10223  fincssdom  10277  fin23lem25  10278  fin23lem26  10279  fin1a2s  10368  pwfseqlem4  10617  ltapr  11000  suplem2pr  11008  qsqueeze  13201  ssfzoulel  13763  ssnn0fi  13995  hashbnd  14346  hashclb  14368  hashgt0elex  14411  hashgt12el  14432  hashgt12el2  14433  2mulprm  16710  pc2dvds  16898  infpnlem1  16929  mndpsuppss  18782  odcl2  19588  ufilmax  23947  ufileu  23959  filufint  23960  hausflim  24021  flimfnfcls  24068  alexsubALTlem3  24089  alexsubALTlem4  24090  reconnlem2  24868  lebnumlem3  25005  rrxmvallem  25446  itg1ge0a  25753  itg2seq  25784  m1lgs  27429  nosepon  27706  leadds1im  28057  leadds1  28059  oncutlt  28334  onnolt  28336  bdaypw2n0bndlem  28533  lmieu  28930  axlowdimlem14  29102  usgredg2v  29374  cusgrfilem3  29604  cusgrfi  29605  vtxdgoddnumeven  29700  clwwlknon1sn  30248  ex-natded5.13-2  30564  diffib  32669  ordtconnlem1  34182  eulerpartlemgh  34636  bnj23  34978  nn0prpw  36647  meran1  36735  mh-regprimbi  36869  finxpreclem6  37854  wl-spae  37988  poimirlem32  38115  heiborlem1  38274  riotaclbgBAD  39542  primrootspoweq0  42687  aks6d1c2p2  42700  hashscontpow  42703  aks6d1c5lem1  42717  aks6d1c6lem3  42753  ioin9i8  42788  onsupmaxb  43780  onsupsucismax  43820  tfsconcat0b  43887  relpmin  45492  reclt0  45930  limclr  46193  eu2ndop1stv  47683  requad01  48207  line2ylem  49337  line2xlem  49339