Theorem pm2.61d 172

Description: Deduction eliminating an antecedent. (Contributed by NM, 27-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2013.)

Hypotheses

Ref	Expression
pm2.61d.1	⊢ (𝜑 → (𝜓 → 𝜒))
pm2.61d.2	⊢ (𝜑 → (¬ 𝜓 → 𝜒))

Assertion

Ref	Expression
pm2.61d	⊢ (𝜑 → 𝜒)

Proof of Theorem pm2.61d

Step	Hyp	Ref	Expression
1		pm2.61d.2	. . . 4 ⊢ (𝜑 → (¬ 𝜓 → 𝜒))
2	1	con1d 142	. . 3 ⊢ (𝜑 → (¬ 𝜒 → 𝜓))
3		pm2.61d.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	syld 47	. 2 ⊢ (𝜑 → (¬ 𝜒 → 𝜒))
5	4	pm2.18d 127	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:  pm2.61d1  173  pm2.61d2  174  pm5.21ndd  372  bija  373  pm2.61dan  800  ecase3d  1015  pm2.61dne  3054  ordunidif  6077  dff3  6689  tfindsg  7391  findsg  7424  brtpos  7704  omwordi  7998  omass  8007  nnmwordi  8062  pssnn  8531  frfi  8558  ixpiunwdom  8850  cantnfp1lem3  8937  infxpenlem  9233  infxp  9435  ackbij1lem16  9455  axpowndlem3  9819  pwfseqlem4a  9881  gchina  9919  prlem936  10267  supsrlem  10331  flflp1  12992  hashunx  13560  swrdccat3blem  13944  repswswrd  14003  sumss  14941  fsumss  14942  prodss  15161  fprodss  15162  ruclem2  15445  prmind2  15885  rpexp  15920  fermltl  15977  prmreclem5  16112  ramcl  16221  wunress  16420  divsfval  16676  efgsfo  18624  lt6abl  18769  gsumval3  18781  mdetunilem8  20932  ordtrest2lem  21515  ptpjpre1  21883  fbfinnfr  22153  filufint  22232  ptcmplem2  22365  cphsqrtcl3  23494  ovoliun  23809  voliunlem3  23856  volsup  23860  cxpsqrt  24987  amgm  25270  wilthlem2  25348  sqff1o  25461  chtublem  25489  bposlem1  25562  bposlem3  25564  ostth  25917  clwwisshclwwslemlem  27528  atdmd  29956  atmd2  29958  mdsymlem4  29964  ordtrest2NEWlem  30815  eulerpartlemb  31277  dfon2lem9  32562  nosupbnd1lem1  32735  nn0prpwlem  33197  ltflcei  34327  poimirlem30  34369  lplnexllnN  36151  2llnjaN  36153  paddasslem14  36420  cdleme32le  37034  dgrsub2  39137  iccelpart  42971  lighneallem3  43146  lighneal  43150