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  27419  clwwisshclwwslemlem  29266  atdmd  31651  atmd2  31653  mdsymlem4  31659  ordtrest2NEWlem  32902  eulerpartlemb  33367  fineqvac  34097  dfon2lem9  34763  nn0prpwlem  35207  bj-ismooredr2  35991  ltflcei  36476  poimirlem30  36518  lplnexllnN  38435  2llnjaN  38437  paddasslem14  38704  cdleme32le  39318  dgrsub2  41877  naddgeoa  42145  iccelpart  46101  lighneallem3  46275  lighneal  46279