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  380  bija  381  pm2.61dan  809  ecase3d  1030  ordunidif  6299  dff3  6958  tfindsg  7682  findsg  7720  brtpos  8022  omwordi  8364  omass  8373  nnmwordi  8428  pssnn  8913  pssnnOLD  8969  frfi  8989  ixpiunwdom  9279  cantnfp1lem3  9368  infxpenlem  9700  infxp  9902  ackbij1lem16  9922  axpowndlem3  10286  pwfseqlem4a  10348  gchina  10386  prlem936  10734  supsrlem  10798  flflp1  13455  hashunx  14029  swrdccat3blem  14380  repswswrd  14425  sumss  15364  fsumss  15365  prodss  15585  fprodss  15586  ruclem2  15869  prmind2  16318  rpexp  16355  fermltl  16413  prmreclem5  16549  ramcl  16658  wunress  16886  wunressOLD  16887  divsfval  17175  efgsfo  19260  lt6abl  19411  gsumval3  19423  mdetunilem8  21676  ordtrest2lem  22262  ptpjpre1  22630  fbfinnfr  22900  filufint  22979  ptcmplem2  23112  cphsqrtcl3  24256  ovoliun  24574  voliunlem3  24621  volsup  24625  cxpsqrt  25763  amgm  26045  wilthlem2  26123  sqff1o  26236  chtublem  26264  bposlem1  26337  bposlem3  26339  ostth  26692  clwwisshclwwslemlem  28278  atdmd  30661  atmd2  30663  mdsymlem4  30669  ordtrest2NEWlem  31774  eulerpartlemb  32235  fineqvac  32966  dfon2lem9  33673  nosupbnd1lem1  33838  noinfbnd1lem1  33853  nn0prpwlem  34438  bj-ismooredr2  35208  ltflcei  35692  poimirlem30  35734  lplnexllnN  37505  2llnjaN  37507  paddasslem14  37774  cdleme32le  38388  dgrsub2  40876  iccelpart  44773  lighneallem3  44947  lighneal  44951