Theorem 3ad2ant3 1046

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

Syntax hints:   -> wi 4   /\ w3a 1004

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 1006

This theorem is referenced by:  simp3l  1051  simp3r  1052  simp31  1059  simp32  1060  simp33  1061  simp3ll  1094  simp3lr  1095  simp3rl  1096  simp3rr  1097  simp3l1  1128  simp3l2  1129  simp3l3  1130  simp3r1  1131  simp3r2  1132  simp3r3  1133  simp31l  1146  simp31r  1147  simp32l  1148  simp32r  1149  simp33l  1150  simp33r  1151  simp311  1170  simp312  1171  simp313  1172  simp321  1173  simp322  1174  simp323  1175  simp331  1176  simp332  1177  simp333  1178  3anim123i  1210  3jaao  1344  ceqsalt  2829  ceqsralt  2830  vtoclgft  2854  ifbothdc  3640  ifnebibdc  3651  ssprsseq  3835  tpssi  3842  sotricim  4420  elirr  4639  en2lp  4652  reg3exmidlemwe  4677  sotri2  5134  poltletr  5137  funprg  5380  funtpg  5381  fntpg  5386  funimaexglem  5413  fvun1  5712  ftpg  5838  fsnunf  5854  fsnunfv  5855  caovimo  6216  brtposg  6420  smoel  6466  rdgivallem  6547  frecsuclem  6572  domssr  6951  mapxpen  7034  unsnfi  7111  unsnfidcex  7112  unsnfidcel  7113  sbthlemi4  7159  elfir  7172  updjud  7281  ltsopi  7540  distrnqg  7607  ltmnqg  7621  mulcanenq0ec  7665  distrnq0  7679  prarloclem5  7720  1idprl  7810  1idpru  7811  ltaprg  7839  recexprlemopl  7845  recexprlemopu  7847  recexprlem1ssl  7853  aptipr  7861  ltmprr  7862  cauappcvgprlemlol  7867  cauappcvgprlemupu  7869  caucvgprlemlol  7890  caucvgprlemupu  7892  caucvgprprlemlol  7918  caucvgprprlemupu  7920  readdcan  8319  cnegexlem2  8355  addcan2  8360  ltadd2  8599  apreap  8767  ltmul1  8772  apcotr  8787  apadd1  8788  mulext1  8792  divdirap  8877  divcanap5  8894  ltdiv1  9048  lt2halves  9380  zdivmul  9570  eluzsub  9786  ledivge1le  9961  addlelt  10003  xaddass  10104  xleadd1  10110  xltadd1  10111  elioo5  10168  iccsupr  10201  iccneg  10224  icoshft  10225  icoshftf1o  10226  zltaddlt1le  10242  fzen  10278  elfz1b  10325  fzrevral  10340  fzshftral  10343  elfz0ubfz0  10360  elfz0fzfz0  10361  fz0fzelfz0  10362  fz0fzdiffz0  10365  elfzo  10384  fzodcel  10388  elfzonlteqm1  10456  modqaddmulmod  10654  expdivap  10853  leexp2a  10855  bcval3  11014  omgadd  11066  ccatval1  11178  ccatval2  11179  ccatval3  11180  ccatass  11189  ccats1val2  11221  swrdval2  11236  swrdlen  11237  pfxfv  11269  pfxnd  11274  pfxsuffeqwrdeq  11283  swrdswrdlem  11289  swrdswrd  11290  pfxswrd  11291  pfxpfx  11293  ccats1pfxeq  11299  ccats1pfxeqrex  11300  pfxccatin12lem2  11316  pfxccatpfx1  11321  swrdccat3b  11325  pfxccatid  11326  shftfibg  11398  elicc4abs  11672  xrmaxltsup  11836  xrmaxadd  11839  xrlemininf  11849  xrminltinf  11850  mulcn2  11890  fsumsplitsnun  11998  prodfrecap  12125  demoivreALT  12353  dvdsval2  12369  dvdsmodexp  12374  dvdsmulcr  12400  modmulconst  12402  dvdsexp  12440  oddge22np1  12460  modremain  12508  mulgcd  12605  mulgcdr  12607  gcddiv  12608  rpmulgcd  12615  rplpwr  12616  coprmdvds  12682  cncongr1  12693  dvdsnprmd  12715  prmexpb  12741  rpexp  12743  cncongrprm  12747  modprm0  12845  modprmn0modprm0  12847  coprimeprodsq  12848  pythagtriplem1  12856  pythagtriplem3  12858  pythagtriplem10  12860  pythagtriplem6  12861  pythagtriplem11  12865  pythagtriplem12  12866  pythagtriplem13  12867  pythagtriplem15  12869  pythagtriplem17  12871  pythagtriplem19  12873  pcdvdsb  12911  dvdsprmpweqle  12928  pcfaclem  12940  isstructr  13115  setsvala  13131  setsresg  13138  strle3g  13209  imasaddvallemg  13416  fvprif  13444  mgmsscl  13462  insubm  13586  dfgrp3mlem  13699  mulgdirlem  13758  mulgp1  13760  mulgmodid  13766  eqglact  13830  rngdi  13972  rngdir  13973  rmodislmodlem  14383  rmodislmod  14384  lssclg  14397  2idlcpblrng  14556  qusmulrng  14565  clsss  14861  ntrcls0  14874  neiss  14893  neipsm  14897  cnpnei  14962  cncnp2m  14974  cnconst2  14976  sslm  14990  upxp  15015  txmetcn  15262  ptolemy  15567  sincosq1eq  15582  rplogbval  15688  rpcxplogb  15707  lgsdirprm  15782  lgsdirnn0  15795  gausslemma2dlem1a  15806  gausslemma2dlem3  15811  2lgslem1a1  15834  2lgsoddprmlem1  15853  2lgsoddprmlem2  15854  structiedg0val  15910  lpvtx  15949  incistruhgr  15960  upgredg2vtx  16018  upgredgpr  16019  ausgrumgrien  16040  ausgrusgrien  16041  ushgredgedg  16096  ushgredgedgloop  16098  uhgrissubgr  16131  egrsubgr  16133  0uhgrsubgr  16135  wlkvtxeledgg  16214  wlkeq  16224  wlkl1loop  16228  uspgr2wlkeq  16235  uspgr2wlkeq2  16236  wlkres  16249  loopclwwlkn1b  16289  clwwlkext2edg  16292  clwwlknonex2lem2  16308  clwwlknonex2  16309  clwwlknun  16311  eupth2lem3lem6fi  16341  findset  16591