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  381  bija  382  pm2.61dan  812  ecase3d  1033  ordunidif  6414  dff3  7102  tfindsg  7850  findsg  7890  brtpos  8220  omwordi  8571  omass  8580  nnmwordi  8635  pssnn  9168  pssnnOLD  9265  frfi  9288  ixpiunwdom  9585  cantnfp1lem3  9675  infxpenlem  10008  infxp  10210  ackbij1lem16  10230  axpowndlem3  10594  pwfseqlem4a  10656  gchina  10694  prlem936  11042  supsrlem  11106  flflp1  13772  hashunx  14346  swrdccat3blem  14689  repswswrd  14734  sumss  15670  fsumss  15671  prodss  15891  fprodss  15892  ruclem2  16175  prmind2  16622  rpexp  16659  fermltl  16717  prmreclem5  16853  ramcl  16962  wunress  17195  wunressOLD  17196  divsfval  17493  efgsfo  19607  lt6abl  19763  gsumval3  19775  mdetunilem8  22121  ordtrest2lem  22707  ptpjpre1  23075  fbfinnfr  23345  filufint  23424  ptcmplem2  23557  cphsqrtcl3  24704  ovoliun  25022  voliunlem3  25069  volsup  25073  cxpsqrt  26211  amgm  26495  wilthlem2  26573  sqff1o  26686  chtublem  26714  bposlem1  26787  bposlem3  26789  ostth  27142  nosupbnd1lem1  27211  noinfbnd1lem1  27226  cutlt  27421  clwwisshclwwslemlem  29297  atdmd  31682  atmd2  31684  mdsymlem4  31690  ordtrest2NEWlem  32933  eulerpartlemb  33398  fineqvac  34128  dfon2lem9  34794  nn0prpwlem  35255  bj-ismooredr2  36039  ltflcei  36524  poimirlem30  36566  lplnexllnN  38483  2llnjaN  38485  paddasslem14  38752  cdleme32le  39366  dgrsub2  41925  naddgeoa  42193  iccelpart  46149  lighneallem3  46323  lighneal  46327