Theorem 3ad2ant3 1004

Description: Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)

Hypothesis

Ref	Expression
3ad2ant.1	|- ( ph -> ch )

Assertion

Ref	Expression
3ad2ant3	|- ( ( ps /\ th /\ ph ) -> ch )

Proof of Theorem 3ad2ant3

Step	Hyp	Ref	Expression
1		3ad2ant.1	. . 3 |- ( ph -> ch )
2	1	adantl 275	. 2 |- ( ( th /\ ph ) -> ch )
3	2	3adant1 999	1 |- ( ( ps /\ th /\ ph ) -> ch )

Syntax hints:   -> wi 4   /\ w3a 962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  simp3l  1009  simp3r  1010  simp31  1017  simp32  1018  simp33  1019  simp3ll  1052  simp3lr  1053  simp3rl  1054  simp3rr  1055  simp3l1  1086  simp3l2  1087  simp3l3  1088  simp3r1  1089  simp3r2  1090  simp3r3  1091  simp31l  1104  simp31r  1105  simp32l  1106  simp32r  1107  simp33l  1108  simp33r  1109  simp311  1128  simp312  1129  simp313  1130  simp321  1131  simp322  1132  simp323  1133  simp331  1134  simp332  1135  simp333  1136  3anim123i  1166  3jaao  1286  ceqsalt  2712  ceqsralt  2713  vtoclgft  2736  ifbothdc  3504  tpssi  3686  sotricim  4245  elirr  4456  en2lp  4469  reg3exmidlemwe  4493  sotri2  4936  poltletr  4939  funprg  5173  funtpg  5174  fntpg  5179  funimaexglem  5206  fvun1  5487  ftpg  5604  fsnunf  5620  fsnunfv  5621  caovimo  5964  brtposg  6151  smoel  6197  rdgivallem  6278  frecsuclem  6303  mapxpen  6742  unsnfi  6807  unsnfidcex  6808  unsnfidcel  6809  sbthlemi4  6848  elfir  6861  updjud  6967  ltsopi  7128  distrnqg  7195  ltmnqg  7209  mulcanenq0ec  7253  distrnq0  7267  prarloclem5  7308  1idprl  7398  1idpru  7399  ltaprg  7427  recexprlemopl  7433  recexprlemopu  7435  recexprlem1ssl  7441  aptipr  7449  ltmprr  7450  cauappcvgprlemlol  7455  cauappcvgprlemupu  7457  caucvgprlemlol  7478  caucvgprlemupu  7480  caucvgprprlemlol  7506  caucvgprprlemupu  7508  readdcan  7902  cnegexlem2  7938  addcan2  7943  ltadd2  8181  apreap  8349  ltmul1  8354  apcotr  8369  apadd1  8370  mulext1  8374  divdirap  8457  divcanap5  8474  ltdiv1  8626  lt2halves  8955  zdivmul  9141  eluzsub  9355  ledivge1le  9513  addlelt  9555  xaddass  9652  xleadd1  9658  xltadd1  9659  elioo5  9716  iccsupr  9749  iccneg  9772  icoshft  9773  icoshftf1o  9774  zltaddlt1le  9789  fzen  9823  elfz1b  9870  fzrevral  9885  fzshftral  9888  elfz0ubfz0  9902  elfz0fzfz0  9903  fz0fzelfz0  9904  fz0fzdiffz0  9907  elfzo  9926  fzodcel  9929  elfzonlteqm1  9987  modqaddmulmod  10164  expdivap  10344  leexp2a  10346  bcval3  10497  omgadd  10548  shftfibg  10592  elicc4abs  10866  xrmaxltsup  11027  xrmaxadd  11030  xrlemininf  11040  xrminltinf  11041  mulcn2  11081  fsumsplitsnun  11188  prodfrecap  11315  demoivreALT  11480  dvdsval2  11496  dvdsmulcr  11523  modmulconst  11525  dvdsexp  11559  oddge22np1  11578  modremain  11626  mulgcd  11704  mulgcdr  11706  gcddiv  11707  rpmulgcd  11714  rplpwr  11715  coprmdvds  11773  cncongr1  11784  dvdsnprmd  11806  prmexpb  11829  rpexp  11831  cncongrprm  11835  isstructr  11974  setsvala  11990  setsresg  11997  strle3g  12051  clsss  12287  ntrcls0  12300  neiss  12319  neipsm  12323  cnpnei  12388  cncnp2m  12400  cnconst2  12402  sslm  12416  upxp  12441  txmetcn  12688  ptolemy  12905  sincosq1eq  12920  findset  13143