Theorem pm2.61d 179

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 145	. . 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  180  pm2.61d2  181  pm5.21ndd  379  bija  380  pm2.61dan  813  ecase3d  1034  ordunidif  6435  dff3  7120  tfindsg  7882  findsg  7920  brtpos  8259  omwordi  8608  omass  8617  nnmwordi  8672  pssnn  9207  frfi  9319  ixpiunwdom  9628  cantnfp1lem3  9718  infxpenlem  10051  infxp  10252  ackbij1lem16  10272  axpowndlem3  10637  pwfseqlem4a  10699  gchina  10737  prlem936  11085  supsrlem  11149  flflp1  13844  hashunx  14422  swrdccat3blem  14774  repswswrd  14819  sumss  15757  fsumss  15758  prodss  15980  fprodss  15981  ruclem2  16265  prmind2  16719  rpexp  16756  fermltl  16818  prmreclem5  16954  ramcl  17063  wunress  17296  wunressOLD  17297  divsfval  17594  efgsfo  19772  lt6abl  19928  gsumval3  19940  mdetunilem8  22641  ordtrest2lem  23227  ptpjpre1  23595  fbfinnfr  23865  filufint  23944  ptcmplem2  24077  cphsqrtcl3  25235  ovoliun  25554  voliunlem3  25601  volsup  25605  cxpsqrt  26760  amgm  27049  wilthlem2  27127  sqff1o  27240  chtublem  27270  bposlem1  27343  bposlem3  27345  ostth  27698  nosupbnd1lem1  27768  noinfbnd1lem1  27783  cutlt  27981  clwwisshclwwslemlem  30042  atdmd  32427  atmd2  32429  mdsymlem4  32435  ordtrest2NEWlem  33883  eulerpartlemb  34350  dvelimalcased  35068  dvelimexcased  35070  fineqvac  35090  dfon2lem9  35773  nn0prpwlem  36305  bj-ismooredr2  37093  ltflcei  37595  poimirlem30  37637  lplnexllnN  39547  2llnjaN  39549  paddasslem14  39816  cdleme32le  40430  dgrsub2  43124  naddgeoa  43384  iccelpart  47358  lighneallem3  47532  lighneal  47536