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  1833  rexim  3074  spc2gv  3551  spc3gv  3555  frpoind  6294  soisoi  7268  isomin  7277  riotaclb  7350  extmptsuppeq  8124  mpoxopynvov0g  8150  fsetcdmex  8793  boxcutc  8871  sdomel  9044  onsdominel  9046  preleqALT  9514  frind  9650  cflim2  10161  cfslbn  10165  cofsmo  10167  fincssdom  10221  fin23lem25  10222  fin23lem26  10223  fin1a2s  10312  pwfseqlem4  10560  ltapr  10943  suplem2pr  10951  qsqueeze  13102  ssfzoulel  13662  ssnn0fi  13894  hashbnd  14245  hashclb  14267  hashgt0elex  14310  hashgt12el  14331  hashgt12el2  14332  2mulprm  16606  pc2dvds  16793  infpnlem1  16824  mndpsuppss  18675  odcl2  19479  ufilmax  23823  ufileu  23835  filufint  23836  hausflim  23897  flimfnfcls  23944  alexsubALTlem3  23965  alexsubALTlem4  23966  reconnlem2  24744  lebnumlem3  24890  rrxmvallem  25332  itg1ge0a  25640  itg2seq  25671  m1lgs  27327  nosepon  27605  sleadd1im  27931  sleadd1  27933  onscutlt  28202  onnolt  28204  lmieu  28763  axlowdimlem14  28935  usgredg2v  29207  cusgrfilem3  29438  cusgrfi  29439  vtxdgoddnumeven  29534  clwwlknon1sn  30082  ex-natded5.13-2  30398  diffib  32503  ordtconnlem1  33958  eulerpartlemgh  34412  bnj23  34751  nn0prpw  36388  meran1  36476  finxpreclem6  37461  wl-spae  37586  poimirlem32  37712  heiborlem1  37871  riotaclbgBAD  39073  primrootspoweq0  42219  aks6d1c2p2  42232  hashscontpow  42235  aks6d1c5lem1  42249  aks6d1c6lem3  42285  ioin9i8  42320  onsupmaxb  43356  onsupsucismax  43396  tfsconcat0b  43463  relpmin  45069  reclt0  45513  limclr  45777  eu2ndop1stv  47249  requad01  47745  line2ylem  48876  line2xlem  48878