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  1829  rexim  3085  spc2gv  3600  spc3gv  3604  frpoind  6365  wfiOLD  6374  soisoi  7348  isomin  7357  riotaclb  7429  extmptsuppeq  8212  mpoxopynvov0g  8238  fsetcdmex  8902  boxcutc  8980  sdomel  9163  onsdominel  9165  preleqALT  9655  frind  9788  cflim2  10301  cfslbn  10305  cofsmo  10307  fincssdom  10361  fin23lem25  10362  fin23lem26  10363  fin1a2s  10452  pwfseqlem4  10700  ltapr  11083  suplem2pr  11091  qsqueeze  13240  ssfzoulel  13796  ssnn0fi  14023  hashbnd  14372  hashclb  14394  hashgt0elex  14437  hashgt12el  14458  hashgt12el2  14459  2mulprm  16727  pc2dvds  16913  infpnlem1  16944  mndpsuppss  18791  odcl2  19598  ufilmax  23931  ufileu  23943  filufint  23944  hausflim  24005  flimfnfcls  24052  alexsubALTlem3  24073  alexsubALTlem4  24074  reconnlem2  24863  lebnumlem3  25009  rrxmvallem  25452  itg1ge0a  25761  itg2seq  25792  m1lgs  27447  nosepon  27725  sleadd1im  28035  sleadd1  28037  lmieu  28807  axlowdimlem14  28985  usgredg2v  29259  cusgrfilem3  29490  cusgrfi  29491  vtxdgoddnumeven  29586  clwwlknon1sn  30129  ex-natded5.13-2  30445  diffib  32549  ordtconnlem1  33885  eulerpartlemgh  34360  bnj23  34711  nn0prpw  36306  meran1  36394  finxpreclem6  37379  wl-spae  37502  poimirlem32  37639  heiborlem1  37798  riotaclbgBAD  38936  primrootspoweq0  42088  aks6d1c2p2  42101  hashscontpow  42104  aks6d1c5lem1  42118  aks6d1c6lem3  42154  ioin9i8  42226  onsupmaxb  43228  onsupsucismax  43269  tfsconcat0b  43336  reclt0  45341  limclr  45611  eu2ndop1stv  47075  requad01  47546  line2ylem  48601  line2xlem  48603