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  226  con4bid  317  aleximi  1835  rexim  3088  spc2gv  3591  spc3gv  3595  frpoind  6344  wfiOLD  6353  soisoi  7325  isomin  7334  riotaclb  7407  extmptsuppeq  8173  mpoxopynvov0g  8199  fsetcdmex  8857  boxcutc  8935  sdomel  9124  onsdominel  9126  preleqALT  9612  frind  9745  cflim2  10258  cfslbn  10262  cofsmo  10264  fincssdom  10318  fin23lem25  10319  fin23lem26  10320  fin1a2s  10409  pwfseqlem4  10657  ltapr  11040  suplem2pr  11048  qsqueeze  13180  ssfzoulel  13726  ssnn0fi  13950  hashbnd  14296  hashclb  14318  hashgt0elex  14361  hashgt12el  14382  hashgt12el2  14383  2mulprm  16630  pc2dvds  16812  infpnlem1  16843  odcl2  19433  ufilmax  23411  ufileu  23423  filufint  23424  hausflim  23485  flimfnfcls  23532  alexsubALTlem3  23553  alexsubALTlem4  23554  reconnlem2  24343  lebnumlem3  24479  rrxmvallem  24921  itg1ge0a  25229  itg2seq  25260  m1lgs  26891  nosepon  27168  sleadd1im  27470  sleadd1  27472  lmieu  28035  axlowdimlem14  28213  usgredg2v  28484  cusgrfilem3  28714  cusgrfi  28715  vtxdgoddnumeven  28810  clwwlknon1sn  29353  ex-natded5.13-2  29669  diffib  31759  ordtconnlem1  32904  eulerpartlemgh  33377  bnj23  33729  nn0prpw  35208  meran1  35296  finxpreclem6  36277  wl-spae  36390  poimirlem32  36520  heiborlem1  36679  riotaclbgBAD  37824  aks6d1c2p2  40957  ioin9i8  41024  onsupmaxb  41988  onsupsucismax  42029  tfsconcat0b  42096  reclt0  44101  limclr  44371  eu2ndop1stv  45833  requad01  46289  mndpsuppss  47047  line2ylem  47437  line2xlem  47439