Theorem pm2.61d 181

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 147	. . 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  182  pm2.61d2  183  pm5.21ndd  383  bija  384  pm2.61dan  811  ecase3d  1029  pm2.61dne  3103  ordunidif  6239  dff3  6866  tfindsg  7575  findsg  7609  brtpos  7901  omwordi  8197  omass  8206  nnmwordi  8261  pssnn  8736  frfi  8763  ixpiunwdom  9055  cantnfp1lem3  9143  infxpenlem  9439  infxp  9637  ackbij1lem16  9657  axpowndlem3  10021  pwfseqlem4a  10083  gchina  10121  prlem936  10469  supsrlem  10533  flflp1  13178  hashunx  13748  swrdccat3blem  14101  repswswrd  14146  sumss  15081  fsumss  15082  prodss  15301  fprodss  15302  ruclem2  15585  prmind2  16029  rpexp  16064  fermltl  16121  prmreclem5  16256  ramcl  16365  wunress  16564  divsfval  16820  efgsfo  18865  lt6abl  19015  gsumval3  19027  mdetunilem8  21228  ordtrest2lem  21811  ptpjpre1  22179  fbfinnfr  22449  filufint  22528  ptcmplem2  22661  cphsqrtcl3  23791  ovoliun  24106  voliunlem3  24153  volsup  24157  cxpsqrt  25286  amgm  25568  wilthlem2  25646  sqff1o  25759  chtublem  25787  bposlem1  25860  bposlem3  25862  ostth  26215  clwwisshclwwslemlem  27791  atdmd  30175  atmd2  30177  mdsymlem4  30183  ordtrest2NEWlem  31165  eulerpartlemb  31626  dfon2lem9  33036  nosupbnd1lem1  33208  nn0prpwlem  33670  bj-ismooredr2  34405  ltflcei  34895  poimirlem30  34937  lplnexllnN  36715  2llnjaN  36717  paddasslem14  36984  cdleme32le  37598  dgrsub2  39784  iccelpart  43642  lighneallem3  43821  lighneal  43825