Theorem 3ad2ant3 1044

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 277	. 2 |- ( ( th /\ ph ) -> ch )
3	2	3adant1 1039	1 |- ( ( ps /\ th /\ ph ) -> ch )

Syntax hints:   -> wi 4   /\ w3a 1002

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

This theorem depends on definitions:  df-bi 117  df-3an 1004

This theorem is referenced by:  simp3l  1049  simp3r  1050  simp31  1057  simp32  1058  simp33  1059  simp3ll  1092  simp3lr  1093  simp3rl  1094  simp3rr  1095  simp3l1  1126  simp3l2  1127  simp3l3  1128  simp3r1  1129  simp3r2  1130  simp3r3  1131  simp31l  1144  simp31r  1145  simp32l  1146  simp32r  1147  simp33l  1148  simp33r  1149  simp311  1168  simp312  1169  simp313  1170  simp321  1171  simp322  1172  simp323  1173  simp331  1174  simp332  1175  simp333  1176  3anim123i  1208  3jaao  1342  ceqsalt  2826  ceqsralt  2827  vtoclgft  2851  ifbothdc  3637  ifnebibdc  3648  ssprsseq  3830  tpssi  3837  sotricim  4414  elirr  4633  en2lp  4646  reg3exmidlemwe  4671  sotri2  5126  poltletr  5129  funprg  5371  funtpg  5372  fntpg  5377  funimaexglem  5404  fvun1  5700  ftpg  5823  fsnunf  5839  fsnunfv  5840  caovimo  6199  brtposg  6400  smoel  6446  rdgivallem  6527  frecsuclem  6552  domssr  6929  mapxpen  7009  unsnfi  7081  unsnfidcex  7082  unsnfidcel  7083  sbthlemi4  7127  elfir  7140  updjud  7249  ltsopi  7507  distrnqg  7574  ltmnqg  7588  mulcanenq0ec  7632  distrnq0  7646  prarloclem5  7687  1idprl  7777  1idpru  7778  ltaprg  7806  recexprlemopl  7812  recexprlemopu  7814  recexprlem1ssl  7820  aptipr  7828  ltmprr  7829  cauappcvgprlemlol  7834  cauappcvgprlemupu  7836  caucvgprlemlol  7857  caucvgprlemupu  7859  caucvgprprlemlol  7885  caucvgprprlemupu  7887  readdcan  8286  cnegexlem2  8322  addcan2  8327  ltadd2  8566  apreap  8734  ltmul1  8739  apcotr  8754  apadd1  8755  mulext1  8759  divdirap  8844  divcanap5  8861  ltdiv1  9015  lt2halves  9347  zdivmul  9537  eluzsub  9752  ledivge1le  9922  addlelt  9964  xaddass  10065  xleadd1  10071  xltadd1  10072  elioo5  10129  iccsupr  10162  iccneg  10185  icoshft  10186  icoshftf1o  10187  zltaddlt1le  10203  fzen  10239  elfz1b  10286  fzrevral  10301  fzshftral  10304  elfz0ubfz0  10321  elfz0fzfz0  10322  fz0fzelfz0  10323  fz0fzdiffz0  10326  elfzo  10345  fzodcel  10349  elfzonlteqm1  10416  modqaddmulmod  10613  expdivap  10812  leexp2a  10814  bcval3  10973  omgadd  11024  ccatval1  11132  ccatval2  11133  ccatval3  11134  ccatass  11143  ccats1val2  11171  swrdval2  11183  swrdlen  11184  pfxfv  11216  pfxnd  11221  pfxsuffeqwrdeq  11230  swrdswrdlem  11236  swrdswrd  11237  pfxswrd  11238  pfxpfx  11240  ccats1pfxeq  11246  ccats1pfxeqrex  11247  pfxccatin12lem2  11263  pfxccatpfx1  11268  swrdccat3b  11272  pfxccatid  11273  shftfibg  11331  elicc4abs  11605  xrmaxltsup  11769  xrmaxadd  11772  xrlemininf  11782  xrminltinf  11783  mulcn2  11823  fsumsplitsnun  11930  prodfrecap  12057  demoivreALT  12285  dvdsval2  12301  dvdsmodexp  12306  dvdsmulcr  12332  modmulconst  12334  dvdsexp  12372  oddge22np1  12392  modremain  12440  mulgcd  12537  mulgcdr  12539  gcddiv  12540  rpmulgcd  12547  rplpwr  12548  coprmdvds  12614  cncongr1  12625  dvdsnprmd  12647  prmexpb  12673  rpexp  12675  cncongrprm  12679  modprm0  12777  modprmn0modprm0  12779  coprimeprodsq  12780  pythagtriplem1  12788  pythagtriplem3  12790  pythagtriplem10  12792  pythagtriplem6  12793  pythagtriplem11  12797  pythagtriplem12  12798  pythagtriplem13  12799  pythagtriplem15  12801  pythagtriplem17  12803  pythagtriplem19  12805  pcdvdsb  12843  dvdsprmpweqle  12860  pcfaclem  12872  isstructr  13047  setsvala  13063  setsresg  13070  strle3g  13141  imasaddvallemg  13348  fvprif  13376  mgmsscl  13394  insubm  13518  dfgrp3mlem  13631  mulgdirlem  13690  mulgp1  13692  mulgmodid  13698  eqglact  13762  rngdi  13903  rngdir  13904  rmodislmodlem  14314  rmodislmod  14315  lssclg  14328  2idlcpblrng  14487  qusmulrng  14496  clsss  14792  ntrcls0  14805  neiss  14824  neipsm  14828  cnpnei  14893  cncnp2m  14905  cnconst2  14907  sslm  14921  upxp  14946  txmetcn  15193  ptolemy  15498  sincosq1eq  15513  rplogbval  15619  rpcxplogb  15638  lgsdirprm  15713  lgsdirnn0  15726  gausslemma2dlem1a  15737  gausslemma2dlem3  15742  2lgslem1a1  15765  2lgsoddprmlem1  15784  2lgsoddprmlem2  15785  structiedg0val  15841  lpvtx  15879  incistruhgr  15890  upgredg2vtx  15946  upgredgpr  15947  ausgrumgrien  15968  ausgrusgrien  15969  ushgredgedg  16024  ushgredgedgloop  16026  wlkvtxeledgg  16055  wlkeq  16065  wlkl1loop  16069  uspgr2wlkeq  16076  uspgr2wlkeq2  16077  findset  16308