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  3087  spc2gv  3600  spc3gv  3604  frpoind  6363  wfiOLD  6372  soisoi  7348  isomin  7357  riotaclb  7429  extmptsuppeq  8213  mpoxopynvov0g  8239  fsetcdmex  8903  boxcutc  8981  sdomel  9164  onsdominel  9166  preleqALT  9657  frind  9790  cflim2  10303  cfslbn  10307  cofsmo  10309  fincssdom  10363  fin23lem25  10364  fin23lem26  10365  fin1a2s  10454  pwfseqlem4  10702  ltapr  11085  suplem2pr  11093  qsqueeze  13243  ssfzoulel  13799  ssnn0fi  14026  hashbnd  14375  hashclb  14397  hashgt0elex  14440  hashgt12el  14461  hashgt12el2  14462  2mulprm  16730  pc2dvds  16917  infpnlem1  16948  mndpsuppss  18778  odcl2  19583  ufilmax  23915  ufileu  23927  filufint  23928  hausflim  23989  flimfnfcls  24036  alexsubALTlem3  24057  alexsubALTlem4  24058  reconnlem2  24849  lebnumlem3  24995  rrxmvallem  25438  itg1ge0a  25746  itg2seq  25777  m1lgs  27432  nosepon  27710  sleadd1im  28020  sleadd1  28022  lmieu  28792  axlowdimlem14  28970  usgredg2v  29244  cusgrfilem3  29475  cusgrfi  29476  vtxdgoddnumeven  29571  clwwlknon1sn  30119  ex-natded5.13-2  30435  diffib  32540  ordtconnlem1  33923  eulerpartlemgh  34380  bnj23  34732  nn0prpw  36324  meran1  36412  finxpreclem6  37397  wl-spae  37522  poimirlem32  37659  heiborlem1  37818  riotaclbgBAD  38955  primrootspoweq0  42107  aks6d1c2p2  42120  hashscontpow  42123  aks6d1c5lem1  42137  aks6d1c6lem3  42173  ioin9i8  42246  onsupmaxb  43251  onsupsucismax  43292  tfsconcat0b  43359  relpmin  44973  reclt0  45402  limclr  45670  eu2ndop1stv  47137  requad01  47608  line2ylem  48672  line2xlem  48674