Theorem 3ad2ant3 1010

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 1005	1 |- ( ( ps /\ th /\ ph ) -> ch )

Syntax hints:   -> wi 4   /\ w3a 968

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 970

This theorem is referenced by:  simp3l  1015  simp3r  1016  simp31  1023  simp32  1024  simp33  1025  simp3ll  1058  simp3lr  1059  simp3rl  1060  simp3rr  1061  simp3l1  1092  simp3l2  1093  simp3l3  1094  simp3r1  1095  simp3r2  1096  simp3r3  1097  simp31l  1110  simp31r  1111  simp32l  1112  simp32r  1113  simp33l  1114  simp33r  1115  simp311  1134  simp312  1135  simp313  1136  simp321  1137  simp322  1138  simp323  1139  simp331  1140  simp332  1141  simp333  1142  3anim123i  1174  3jaao  1298  ceqsalt  2752  ceqsralt  2753  vtoclgft  2776  ifbothdc  3552  tpssi  3739  sotricim  4301  elirr  4518  en2lp  4531  reg3exmidlemwe  4556  sotri2  5001  poltletr  5004  funprg  5238  funtpg  5239  fntpg  5244  funimaexglem  5271  fvun1  5552  ftpg  5669  fsnunf  5685  fsnunfv  5686  caovimo  6035  brtposg  6222  smoel  6268  rdgivallem  6349  frecsuclem  6374  mapxpen  6814  unsnfi  6884  unsnfidcex  6885  unsnfidcel  6886  sbthlemi4  6925  elfir  6938  updjud  7047  ltsopi  7261  distrnqg  7328  ltmnqg  7342  mulcanenq0ec  7386  distrnq0  7400  prarloclem5  7441  1idprl  7531  1idpru  7532  ltaprg  7560  recexprlemopl  7566  recexprlemopu  7568  recexprlem1ssl  7574  aptipr  7582  ltmprr  7583  cauappcvgprlemlol  7588  cauappcvgprlemupu  7590  caucvgprlemlol  7611  caucvgprlemupu  7613  caucvgprprlemlol  7639  caucvgprprlemupu  7641  readdcan  8038  cnegexlem2  8074  addcan2  8079  ltadd2  8317  apreap  8485  ltmul1  8490  apcotr  8505  apadd1  8506  mulext1  8510  divdirap  8593  divcanap5  8610  ltdiv1  8763  lt2halves  9092  zdivmul  9281  eluzsub  9495  ledivge1le  9662  addlelt  9704  xaddass  9805  xleadd1  9811  xltadd1  9812  elioo5  9869  iccsupr  9902  iccneg  9925  icoshft  9926  icoshftf1o  9927  zltaddlt1le  9943  fzen  9978  elfz1b  10025  fzrevral  10040  fzshftral  10043  elfz0ubfz0  10060  elfz0fzfz0  10061  fz0fzelfz0  10062  fz0fzdiffz0  10065  elfzo  10084  fzodcel  10087  elfzonlteqm1  10145  modqaddmulmod  10326  expdivap  10506  leexp2a  10508  bcval3  10664  omgadd  10715  shftfibg  10762  elicc4abs  11036  xrmaxltsup  11199  xrmaxadd  11202  xrlemininf  11212  xrminltinf  11213  mulcn2  11253  fsumsplitsnun  11360  prodfrecap  11487  demoivreALT  11714  dvdsval2  11730  dvdsmodexp  11735  dvdsmulcr  11761  modmulconst  11763  dvdsexp  11799  oddge22np1  11818  modremain  11866  mulgcd  11949  mulgcdr  11951  gcddiv  11952  rpmulgcd  11959  rplpwr  11960  coprmdvds  12024  cncongr1  12035  dvdsnprmd  12057  prmexpb  12083  rpexp  12085  cncongrprm  12089  modprm0  12186  modprmn0modprm0  12188  coprimeprodsq  12189  pythagtriplem1  12197  pythagtriplem3  12199  pythagtriplem10  12201  pythagtriplem6  12202  pythagtriplem11  12206  pythagtriplem12  12207  pythagtriplem13  12208  pythagtriplem15  12210  pythagtriplem17  12212  pythagtriplem19  12214  pcdvdsb  12251  dvdsprmpweqle  12268  pcfaclem  12279  isstructr  12409  setsvala  12425  setsresg  12432  strle3g  12487  mgmsscl  12592  clsss  12758  ntrcls0  12771  neiss  12790  neipsm  12794  cnpnei  12859  cncnp2m  12871  cnconst2  12873  sslm  12887  upxp  12912  txmetcn  13159  ptolemy  13385  sincosq1eq  13400  rplogbval  13503  rpcxplogb  13522  lgsdirprm  13575  lgsdirnn0  13588  findset  13827