Theorem pm2.61d 181

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 146	. . 3 ⊢ (𝜑 → (¬ 𝜒 → 𝜓))
3		pm2.61d.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	syld 48	. 2 ⊢ (𝜑 → (¬ 𝜒 → 𝜒))
5	4	pm2.18d 128	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  pm2.61d1  182  pm2.61d2  183  pm5.21ndd  382  bija  383  pm2.61dan  825  ecase3d  1050  ordunidif  6406  dff3  7092  tfindsg  7861  findsg  7898  brtpos  8236  omwordi  8563  omass  8572  nnmwordi  8628  pssnn  9168  frfi  9260  ixpiunwdom  9568  cantnfp1lem3  9665  infxpenlem  10073  infxp  10273  ackbij1lem16  10293  axpowndlem3  10665  pwfseqlem4a  10727  gchina  10765  prlem936  11113  supsrlem  11177  flflp1  13927  hashunx  14510  swrdccat3blem  14868  repswswrd  14915  sumss  15870  fsumss  15871  prodss  16094  fprodss  16095  ruclem2  16380  prmind2  16840  rpexp  16878  fermltl  16941  prmreclem5  17078  ramcl  17187  wunress  17407  divsfval  17699  efgsfo  19933  lt6abl  20089  gsumval3  20101  mdetunilem8  22914  ordtrest2lem  23501  ptpjpre1  23870  fbfinnfr  24140  filufint  24219  ptcmplem2  24352  cphsqrtcl3  25488  ovoliun  25806  voliunlem3  25853  volsup  25857  cxpsqrt  27013  amgm  27300  wilthlem2  27378  sqff1o  27491  chtublem  27520  bposlem1  27593  bposlem3  27595  ostth  27948  nosupbnd1lem1  28047  noinfbnd1lem1  28062  cutlt  28300  clwwisshclwwslemlem  30586  atdmd  32982  atmd2  32984  mdsymlem4  32990  ordtrest2NEWlem  34536  eulerpartlemb  34983  dvelimalcased  35688  dvelimexcased  35690  fineqvac  35757  fineqvnttrclselem1  35762  dfon2lem9  36523  nn0prpwlem  37080  axtcond  37236  bj-ismooredr2  37999  ltflcei  38499  poimirlem30  38536  lplnexllnN  40589  2llnjaN  40591  paddasslem14  40858  cdleme32le  41472  dgrsub2  44095  naddgeoa  44354  evenwodadd  47855  iccelpart  48459  lighneallem3  48636  lighneal  48640  prmringnzring  49378