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  6418  dff3  7102  tfindsg  7866  findsg  7903  brtpos  8240  omwordi  8565  omass  8574  nnmwordi  8630  pssnn  9163  frfi  9255  ixpiunwdom  9562  cantnfp1lem3  9659  infxpenlem  10016  infxp  10216  ackbij1lem16  10236  axpowndlem3  10602  pwfseqlem4a  10664  gchina  10702  prlem936  11050  supsrlem  11114  flflp1  13860  hashunx  14442  swrdccat3blem  14800  repswswrd  14847  sumss  15801  fsumss  15802  prodss  16027  fprodss  16028  ruclem2  16313  prmind2  16768  rpexp  16806  fermltl  16868  prmreclem5  17005  ramcl  17114  wunress  17334  divsfval  17626  efgsfo  19840  lt6abl  19996  gsumval3  20008  mdetunilem8  22813  ordtrest2lem  23397  ptpjpre1  23765  fbfinnfr  24035  filufint  24114  ptcmplem2  24247  cphsqrtcl3  25383  ovoliun  25701  voliunlem3  25748  volsup  25752  cxpsqrt  26905  amgm  27192  wilthlem2  27270  sqff1o  27383  chtublem  27412  bposlem1  27485  bposlem3  27487  ostth  27840  nosupbnd1lem1  27909  noinfbnd1lem1  27924  cutlt  28162  clwwisshclwwslemlem  30401  atdmd  32787  atmd2  32789  mdsymlem4  32795  ordtrest2NEWlem  34343  eulerpartlemb  34790  dvelimalcased  35495  dvelimexcased  35497  fineqvac  35553  fineqvnttrclselem1  35558  dfon2lem9  36302  nn0prpwlem  36874  axtcond  37030  bj-ismooredr2  37793  ltflcei  38300  poimirlem30  38342  lplnexllnN  40379  2llnjaN  40381  paddasslem14  40648  cdleme32le  41262  dgrsub2  43903  naddgeoa  44162  evenwodadd  47643  iccelpart  48223  lighneallem3  48400  lighneal  48404  prmringnzring  49143