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  6410  dff3  7097  tfindsg  7845  findsg  7885  brtpos  8215  omwordi  8567  omass  8576  nnmwordi  8631  pssnn  9164  pssnnOLD  9261  frfi  9284  ixpiunwdom  9581  cantnfp1lem3  9671  infxpenlem  10004  infxp  10206  ackbij1lem16  10226  axpowndlem3  10590  pwfseqlem4a  10652  gchina  10690  prlem936  11038  supsrlem  11102  flflp1  13768  hashunx  14342  swrdccat3blem  14685  repswswrd  14730  sumss  15666  fsumss  15667  prodss  15887  fprodss  15888  ruclem2  16171  prmind2  16618  rpexp  16655  fermltl  16713  prmreclem5  16849  ramcl  16958  wunress  17191  wunressOLD  17192  divsfval  17489  efgsfo  19600  lt6abl  19755  gsumval3  19767  mdetunilem8  22103  ordtrest2lem  22689  ptpjpre1  23057  fbfinnfr  23327  filufint  23406  ptcmplem2  23539  cphsqrtcl3  24686  ovoliun  25004  voliunlem3  25051  volsup  25055  cxpsqrt  26193  amgm  26475  wilthlem2  26553  sqff1o  26666  chtublem  26694  bposlem1  26767  bposlem3  26769  ostth  27122  nosupbnd1lem1  27191  noinfbnd1lem1  27206  cutlt  27399  clwwisshclwwslemlem  29246  atdmd  31629  atmd2  31631  mdsymlem4  31637  ordtrest2NEWlem  32840  eulerpartlemb  33305  fineqvac  34035  dfon2lem9  34701  nn0prpwlem  35145  bj-ismooredr2  35929  ltflcei  36414  poimirlem30  36456  lplnexllnN  38373  2llnjaN  38375  paddasslem14  38642  cdleme32le  39256  dgrsub2  41810  naddgeoa  42078  iccelpart  46036  lighneallem3  46210  lighneal  46214