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  6411  dff3  7099  tfindsg  7847  findsg  7887  brtpos  8217  omwordi  8568  omass  8577  nnmwordi  8632  pssnn  9165  pssnnOLD  9262  frfi  9285  ixpiunwdom  9582  cantnfp1lem3  9672  infxpenlem  10005  infxp  10207  ackbij1lem16  10227  axpowndlem3  10591  pwfseqlem4a  10653  gchina  10691  prlem936  11039  supsrlem  11103  flflp1  13769  hashunx  14343  swrdccat3blem  14686  repswswrd  14731  sumss  15667  fsumss  15668  prodss  15888  fprodss  15889  ruclem2  16172  prmind2  16619  rpexp  16656  fermltl  16714  prmreclem5  16850  ramcl  16959  wunress  17192  wunressOLD  17193  divsfval  17490  efgsfo  19602  lt6abl  19758  gsumval3  19770  mdetunilem8  22113  ordtrest2lem  22699  ptpjpre1  23067  fbfinnfr  23337  filufint  23416  ptcmplem2  23549  cphsqrtcl3  24696  ovoliun  25014  voliunlem3  25061  volsup  25065  cxpsqrt  26203  amgm  26485  wilthlem2  26563  sqff1o  26676  chtublem  26704  bposlem1  26777  bposlem3  26779  ostth  27132  nosupbnd1lem1  27201  noinfbnd1lem1  27216  cutlt  27409  clwwisshclwwslemlem  29256  atdmd  31639  atmd2  31641  mdsymlem4  31647  ordtrest2NEWlem  32891  eulerpartlemb  33356  fineqvac  34086  dfon2lem9  34752  nn0prpwlem  35196  bj-ismooredr2  35980  ltflcei  36465  poimirlem30  36507  lplnexllnN  38424  2llnjaN  38426  paddasslem14  38693  cdleme32le  39307  dgrsub2  41863  naddgeoa  42131  iccelpart  46088  lighneallem3  46262  lighneal  46266