Theorem pm2.61d 169

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 138	. . 3 ⊢ (𝜑 → (¬ 𝜒 → 𝜓))
3		pm2.61d.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	syld 46	. 2 ⊢ (𝜑 → (¬ 𝜒 → 𝜒))
5	4	pm2.18d 123	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  170  pm2.61d2  171  pm5.21ndd  368  bija  369  pm2.61dan  828  ecase3d  981  axc11nlemOLD2  1975  axc11nlemOLD  2146  axc11nlemALT  2294  pm2.61dne  2868  ordunidif  5690  dff3  6280  tfindsg  6952  findsg  6985  brtpos  7248  omwordi  7538  omass  7547  nnmwordi  7602  pssnn  8063  frfi  8090  ixpiunwdom  8379  cantnfp1lem3  8460  infxpenlem  8719  infxp  8920  ackbij1lem16  8940  axpowndlem3  9300  pwfseqlem4a  9362  gchina  9400  prlem936  9748  supsrlem  9811  flflp1  12470  hashunx  13036  swrdccat3blem  13346  repswswrd  13382  sumss  14302  fsumss  14303  prodss  14516  fprodss  14517  ruclem2  14800  prmind2  15236  rpexp  15270  fermltl  15327  prmreclem5  15462  ramcl  15571  wunress  15767  divsfval  16030  efgsfo  17975  lt6abl  18119  gsumval3  18131  mdetunilem8  20244  ordtrest2lem  20817  ptpjpre1  21184  fbfinnfr  21455  filufint  21534  ptcmplem2  21667  cphsqrtcl3  22795  ovoliun  23080  voliunlem3  23127  volsup  23131  cxpsqrt  24249  amgm  24517  wilthlem2  24595  sqff1o  24708  chtublem  24736  bposlem1  24809  bposlem3  24811  ostth  25128  clwwisshclwwlem1  26333  atdmd  28641  atmd2  28643  mdsymlem4  28649  ordtrest2NEWlem  29296  eulerpartlemb  29757  dfon2lem9  30940  nn0prpwlem  31487  ltflcei  32567  poimirlem30  32609  lplnexllnN  33868  2llnjaN  33870  paddasslem14  34137  cdleme32le  34753  dgrsub2  36724  iccelpart  39971  lighneallem3  40062  lighneal  40066  clwwisshclwwslemlem  41233