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  1834  rexim  3079  spc2gv  3543  spc3gv  3547  frpoind  6300  soisoi  7276  isomin  7285  riotaclb  7358  extmptsuppeq  8131  mpoxopynvov0g  8157  fsetcdmex  8803  boxcutc  8882  sdomel  9055  onsdominel  9057  preleqALT  9529  frind  9665  cflim2  10176  cfslbn  10180  cofsmo  10182  fincssdom  10236  fin23lem25  10237  fin23lem26  10238  fin1a2s  10327  pwfseqlem4  10576  ltapr  10959  suplem2pr  10967  qsqueeze  13144  ssfzoulel  13706  ssnn0fi  13938  hashbnd  14289  hashclb  14311  hashgt0elex  14354  hashgt12el  14375  hashgt12el2  14376  2mulprm  16653  pc2dvds  16841  infpnlem1  16872  mndpsuppss  18724  odcl2  19531  ufilmax  23882  ufileu  23894  filufint  23895  hausflim  23956  flimfnfcls  24003  alexsubALTlem3  24024  alexsubALTlem4  24025  reconnlem2  24803  lebnumlem3  24940  rrxmvallem  25381  itg1ge0a  25688  itg2seq  25719  m1lgs  27365  nosepon  27643  leadds1im  27993  leadds1  27995  oncutlt  28270  onnolt  28272  bdaypw2n0bndlem  28469  lmieu  28866  axlowdimlem14  29038  usgredg2v  29310  cusgrfilem3  29541  cusgrfi  29542  vtxdgoddnumeven  29637  clwwlknon1sn  30185  ex-natded5.13-2  30501  diffib  32606  ordtconnlem1  34084  eulerpartlemgh  34538  bnj23  34877  nn0prpw  36521  meran1  36609  mh-regprimbi  36743  finxpreclem6  37726  wl-spae  37860  poimirlem32  37987  heiborlem1  38146  riotaclbgBAD  39414  primrootspoweq0  42559  aks6d1c2p2  42572  hashscontpow  42575  aks6d1c5lem1  42589  aks6d1c6lem3  42625  ioin9i8  42660  onsupmaxb  43685  onsupsucismax  43725  tfsconcat0b  43792  relpmin  45397  reclt0  45838  limclr  46101  eu2ndop1stv  47585  requad01  48109  line2ylem  49239  line2xlem  49241