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  812  ecase3d  1034  ordunidif  6407  dff3  7095  tfindsg  7861  findsg  7898  brtpos  8239  omwordi  8588  omass  8597  nnmwordi  8652  pssnn  9187  frfi  9298  ixpiunwdom  9609  cantnfp1lem3  9699  infxpenlem  10032  infxp  10233  ackbij1lem16  10253  axpowndlem3  10618  pwfseqlem4a  10680  gchina  10718  prlem936  11066  supsrlem  11130  flflp1  13829  hashunx  14409  swrdccat3blem  14762  repswswrd  14807  sumss  15745  fsumss  15746  prodss  15968  fprodss  15969  ruclem2  16255  prmind2  16709  rpexp  16746  fermltl  16808  prmreclem5  16945  ramcl  17054  wunress  17275  divsfval  17566  efgsfo  19725  lt6abl  19881  gsumval3  19893  mdetunilem8  22562  ordtrest2lem  23146  ptpjpre1  23514  fbfinnfr  23784  filufint  23863  ptcmplem2  23996  cphsqrtcl3  25144  ovoliun  25463  voliunlem3  25510  volsup  25514  cxpsqrt  26669  amgm  26958  wilthlem2  27036  sqff1o  27149  chtublem  27179  bposlem1  27252  bposlem3  27254  ostth  27607  nosupbnd1lem1  27677  noinfbnd1lem1  27692  cutlt  27897  clwwisshclwwslemlem  29999  atdmd  32384  atmd2  32386  mdsymlem4  32392  ordtrest2NEWlem  33958  eulerpartlemb  34405  dvelimalcased  35111  dvelimexcased  35113  fineqvac  35133  dfon2lem9  35814  nn0prpwlem  36345  bj-ismooredr2  37133  ltflcei  37637  poimirlem30  37679  lplnexllnN  39588  2llnjaN  39590  paddasslem14  39857  cdleme32le  40471  dgrsub2  43134  naddgeoa  43393  evenwodadd  46897  iccelpart  47427  lighneallem3  47601  lighneal  47605