Theorem 3ad2ant3 1051

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

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simp3l  1056  simp3r  1057  simp31  1064  simp32  1065  simp33  1066  simp3ll  1099  simp3lr  1100  simp3rl  1101  simp3rr  1102  simp3l1  1133  simp3l2  1134  simp3l3  1135  simp3r1  1136  simp3r2  1137  simp3r3  1138  simp31l  1151  simp31r  1152  simp32l  1153  simp32r  1154  simp33l  1155  simp33r  1156  simp311  1175  simp312  1176  simp313  1177  simp321  1178  simp322  1179  simp323  1180  simp331  1181  simp332  1182  simp333  1183  3anim123i  1215  3jaao  1349  ceqsalt  2848  ceqsralt  2849  vtoclgft  2873  ifbothdc  3675  ifnebibdc  3686  ssprsseq  3877  tpssi  3884  sotricim  4468  elirr  4688  en2lp  4701  reg3exmidlemwe  4726  sotri2  5185  poltletr  5188  funprg  5431  funtpg  5432  fntpg  5437  funimaexglem  5464  fvun1  5769  ftpg  5899  fsnunf  5915  fsnunfv  5916  caovimo  6283  funsssuppss  6498  brtposg  6525  smoel  6571  rdgivallem  6652  frecsuclem  6677  domssr  7064  mapxpen  7148  unsnfi  7226  unsnfidcex  7227  unsnfidcel  7228  sbthlemi4  7277  elfir  7307  updjud  7422  ltsopi  7687  distrnqg  7754  ltmnqg  7768  mulcanenq0ec  7812  distrnq0  7826  prarloclem5  7867  1idprl  7957  1idpru  7958  ltaprg  7986  recexprlemopl  7992  recexprlemopu  7994  recexprlem1ssl  8000  aptipr  8008  ltmprr  8009  cauappcvgprlemlol  8014  cauappcvgprlemupu  8016  caucvgprlemlol  8037  caucvgprlemupu  8039  caucvgprprlemlol  8065  caucvgprprlemupu  8067  readdcan  8467  cnegexlem2  8503  addcan2  8508  ltadd2  8748  apreap  8917  ltmul1  8922  apcotr  8937  apadd1  8938  mulext1  8942  divdirap  9029  divcanap5  9046  ltdiv1  9200  ind1  9302  ind0  9303  lt2halves  9545  zdivmul  9740  eluzsub  9961  ledivge1le  10137  addlelt  10179  xaddass  10281  xleadd1  10287  xltadd1  10288  elioo5  10345  iccsupr  10378  iccneg  10401  icoshft  10402  icoshftf1o  10403  zltaddlt1le  10420  fzen  10457  elfz1b  10507  fzrevral  10522  fzshftral  10525  elfz0ubfz0  10542  elfz0fzfz0  10543  fz0fzelfz0  10544  fz0fzdiffz0  10547  elfzo  10566  fzodcel  10570  elfzonlteqm1  10638  modqaddmulmod  10841  expdivap  11040  leexp2a  11042  bcval3  11203  omgadd  11256  ccatval1  11379  ccatval2  11380  ccatval3  11381  ccatass  11390  ccats1val2  11422  swrdval2  11437  swrdlen  11438  pfxfv  11470  pfxnd  11475  pfxsuffeqwrdeq  11484  swrdswrdlem  11490  swrdswrd  11491  pfxswrd  11492  pfxpfx  11494  ccats1pfxeq  11500  ccats1pfxeqrex  11501  pfxccatin12lem2  11517  pfxccatpfx1  11522  swrdccat3b  11526  pfxccatid  11527  shftfibg  11599  elicc4abs  11875  xrmaxltsup  12040  xrmaxadd  12043  xrlemininf  12053  xrminltinf  12054  mulcn2  12094  fsumsplitsnun  12202  prodfrecap  12329  demoivreALT  12557  dvdsval2  12573  dvdsmodexp  12578  dvdsmulcr  12604  modmulconst  12606  dvdsexp  12644  oddge22np1  12664  modremain  12712  mulgcd  12809  mulgcdr  12811  gcddiv  12812  rpmulgcd  12819  rplpwr  12820  coprmdvds  12886  cncongr1  12897  dvdsnprmd  12919  prmexpb  12946  rpexp  12948  cncongrprm  12952  modprm0  13053  modprmn0modprm0  13055  coprimeprodsq  13056  pythagtriplem1  13064  pythagtriplem3  13066  pythagtriplem10  13068  pythagtriplem6  13069  pythagtriplem11  13073  pythagtriplem12  13074  pythagtriplem13  13075  pythagtriplem15  13077  pythagtriplem17  13079  pythagtriplem19  13081  pcdvdsb  13119  dvdsprmpweqle  13136  pcfaclem  13148  ballotfilemieq  13309  ballotfilemrv1  13313  isstructr  13416  setsvala  13432  setsresg  13439  strle3g  13511  imasaddvallemg  13685  fvprif  13713  mgmsscl  13730  insubm  13841  dfgrp3mlem  13952  mulgdirlem  14005  mulgp1  14007  mulgmodid  14013  eqglact  14077  gsumconstcmn  14215  rngdi  14288  rngdir  14289  rmodislmodlem  14736  rmodislmod  14737  lssclg  14750  2idlcpblrng  14909  qusmulrng  14918  assa2ass  15058  assa2ass2  15059  psrbagaddclfi  15110  clsss  15268  ntrcls0  15281  neiss  15300  neipsm  15304  cnpnei  15369  cncnp2m  15381  cnconst2  15383  sslm  15397  upxp  15422  txmetcn  15669  ptolemy  15975  sincosq1eq  15990  rplogbval  16100  rpcxplogb  16119  pellexlem1  16148  bcmono  16202  lgsdirprm  16251  lgsdirnn0  16264  gausslemma2dlem1a  16275  gausslemma2dlem3  16280  2lgslem1a1  16303  2lgsoddprmlem1  16322  2lgsoddprmlem2  16323  structiedg0val  16379  lpvtx  16418  incistruhgr  16429  upgredg2vtx  16487  upgredgpr  16488  ausgrumgrien  16509  ausgrusgrien  16510  ushgredgedg  16565  ushgredgedgloop  16567  uhgrissubgr  16600  egrsubgr  16602  0uhgrsubgr  16604  wlkvtxeledgg  16683  wlkeq  16693  wlkl1loop  16697  uspgr2wlkeq  16704  uspgr2wlkeq2  16705  wlkres  16718  loopclwwlkn1b  16758  clwwlkext2edg  16761  clwwlknonex2lem2  16777  clwwlknonex2  16778  clwwlknun  16780  eupth2lem3lem6fi  16810  findset  17069