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  6413  dff3  7101  tfindsg  7873  findsg  7910  brtpos  8256  omwordi  8583  omass  8592  nnmwordi  8648  pssnn  9188  frfi  9280  ixpiunwdom  9588  cantnfp1lem3  9685  infxpenlem  10096  infxp  10296  ackbij1lem16  10316  axpowndlem3  10688  pwfseqlem4a  10750  gchina  10788  prlem936  11136  supsrlem  11200  flflp1  13951  hashunx  14534  swrdccat3blem  14893  repswswrd  14940  sumss  15896  fsumss  15897  prodss  16120  fprodss  16121  ruclem2  16406  prmind2  16866  rpexp  16904  fermltl  16967  prmreclem5  17104  ramcl  17213  wunress  17433  divsfval  17725  efgsfo  19959  lt6abl  20115  gsumval3  20127  mdetunilem8  22940  ordtrest2lem  23527  ptpjpre1  23896  fbfinnfr  24166  filufint  24245  ptcmplem2  24378  cphsqrtcl3  25514  ovoliun  25832  voliunlem3  25879  volsup  25883  cxpsqrt  27037  amgm  27324  wilthlem2  27402  sqff1o  27515  chtublem  27544  bposlem1  27617  bposlem3  27619  ostth  27972  nosupbnd1lem1  28071  noinfbnd1lem1  28086  cutlt  28324  clwwisshclwwslemlem  30610  atdmd  33006  atmd2  33008  mdsymlem4  33014  ordtrest2NEWlem  34601  eulerpartlemb  35047  dvelimalcased  35752  dvelimexcased  35754  fineqvac  35841  fineqvnttrclselem1  35846  dfon2lem9  36646  nn0prpwlem  37203  axtcond  37359  bj-ismooredr2  38124  ltflcei  38625  poimirlem30  38662  lplnexllnN  40715  2llnjaN  40717  paddasslem14  40984  cdleme32le  41598  dgrsub2  44231  naddgeoa  44490  evenwodadd  48005  iccelpart  48609  lighneallem3  48786  lighneal  48790  prmringnzring  49528