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  6434  dff3  7127  tfindsg  7899  findsg  7936  brtpos  8283  omwordi  8610  omass  8619  nnmwordi  8675  pssnn  9215  frfi  9307  ixpiunwdom  9614  cantnfp1lem3  9711  infxpenlem  10122  infxp  10322  ackbij1lem16  10342  axpowndlem3  10714  pwfseqlem4a  10776  gchina  10814  prlem936  11162  supsrlem  11226  flflp1  13977  hashunx  14560  swrdccat3blem  14919  repswswrd  14966  sumss  15922  fsumss  15923  prodss  16146  fprodss  16147  ruclem2  16432  prmind2  16892  rpexp  16930  fermltl  16993  prmreclem5  17130  ramcl  17239  wunress  17459  divsfval  17751  efgsfo  19986  lt6abl  20142  gsumval3  20154  mdetunilem8  22967  ordtrest2lem  23554  ptpjpre1  23923  fbfinnfr  24193  filufint  24272  ptcmplem2  24405  cphsqrtcl3  25541  ovoliun  25859  voliunlem3  25906  volsup  25910  cxpsqrt  27064  amgm  27351  wilthlem2  27429  sqff1o  27542  chtublem  27571  bposlem1  27644  bposlem3  27646  ostth  27999  nosupbnd1lem1  28098  noinfbnd1lem1  28113  cutlt  28351  clwwisshclwwslemlem  30637  atdmd  33033  atmd2  33035  mdsymlem4  33041  ordtrest2NEWlem  34637  eulerpartlemb  35083  dvelimalcased  35788  dvelimexcased  35790  fineqvac  35897  fineqvnttrclselem1  35902  dfon2lem9  36744  nn0prpwlem  37301  axtcond  37457  bj-ismooredr2  38235  ltflcei  38736  poimirlem30  38773  lplnexllnN  40824  2llnjaN  40826  paddasslem14  41093  cdleme32le  41707  dgrsub2  44340  naddgeoa  44599  evenwodadd  48126  iccelpart  48730  lighneallem3  48907  lighneal  48911  prmringnzring  49649