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  pm2.18OLD  129  con2d  136  con1d  147  impcon4bid  229  con4bid  319  norassOLD  1534  aleximi  1832  spc2gv  3601  spc3gv  3605  wfi  6181  soisoi  7081  isomin  7090  riotaclb  7155  extmptsuppeq  7854  mpoxopynvov0g  7880  boxcutc  8505  sdomel  8664  onsdominel  8666  preleqALT  9080  cflim2  9685  cfslbn  9689  cofsmo  9691  fincssdom  9745  fin23lem25  9746  fin23lem26  9747  fin1a2s  9836  pwfseqlem4  10084  ltapr  10467  suplem2pr  10475  qsqueeze  12595  ssfzoulel  13132  ssnn0fi  13354  hashbnd  13697  hashclb  13720  hashgt0elex  13763  hashgt12el  13784  hashgt12el2  13785  2mulprm  16037  pc2dvds  16215  infpnlem1  16246  odcl2  18692  ufilmax  22515  ufileu  22527  filufint  22528  hausflim  22589  flimfnfcls  22636  alexsubALTlem3  22657  alexsubALTlem4  22658  reconnlem2  23435  lebnumlem3  23567  rrxmvallem  24007  itg1ge0a  24312  itg2seq  24343  m1lgs  25964  lmieu  26570  axlowdimlem14  26741  usgredg2v  27009  cusgrfilem3  27239  cusgrfi  27240  vtxdgoddnumeven  27335  clwwlknon1sn  27879  ex-natded5.13-2  28195  ordtconnlem1  31167  eulerpartlemgh  31636  bnj23  31988  frpoind  33080  frind  33085  nosepon  33172  nn0prpw  33671  meran1  33759  finxpreclem6  34680  wl-spae  34776  poimirlem32  34939  heiborlem1  35104  riotaclbgBAD  36105  ioin9i8  39119  reclt0  41683  limclr  41956  eu2ndop1stv  43344  requad01  43806  mndpsuppss  44439  line2ylem  44758  line2xlem  44760