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 )

Syntax hints:   -> wi 4   /\ w3a 1009

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 1011

This theorem is referenced 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  3672  ifnebibdc  3683  ssprsseq  3872  tpssi  3879  sotricim  4463  elirr  4683  en2lp  4696  reg3exmidlemwe  4721  sotri2  5180  poltletr  5183  funprg  5426  funtpg  5427  fntpg  5432  funimaexglem  5459  fvun1  5763  ftpg  5890  fsnunf  5906  fsnunfv  5907  caovimo  6273  funsssuppss  6488  brtposg  6515  smoel  6561  rdgivallem  6642  frecsuclem  6667  domssr  7054  mapxpen  7138  unsnfi  7216  unsnfidcex  7217  unsnfidcel  7218  sbthlemi4  7267  elfir  7297  updjud  7412  ltsopi  7677  distrnqg  7744  ltmnqg  7758  mulcanenq0ec  7802  distrnq0  7816  prarloclem5  7857  1idprl  7947  1idpru  7948  ltaprg  7976  recexprlemopl  7982  recexprlemopu  7984  recexprlem1ssl  7990  aptipr  7998  ltmprr  7999  cauappcvgprlemlol  8004  cauappcvgprlemupu  8006  caucvgprlemlol  8027  caucvgprlemupu  8029  caucvgprprlemlol  8055  caucvgprprlemupu  8057  readdcan  8456  cnegexlem2  8492  addcan2  8497  ltadd2  8737  apreap  8905  ltmul1  8910  apcotr  8925  apadd1  8926  mulext1  8930  divdirap  9017  divcanap5  9034  ltdiv1  9188  lt2halves  9520  zdivmul  9715  eluzsub  9931  ledivge1le  10106  addlelt  10148  xaddass  10250  xleadd1  10256  xltadd1  10257  elioo5  10314  iccsupr  10347  iccneg  10370  icoshft  10371  icoshftf1o  10372  zltaddlt1le  10389  fzen  10426  elfz1b  10475  fzrevral  10490  fzshftral  10493  elfz0ubfz0  10510  elfz0fzfz0  10511  fz0fzelfz0  10512  fz0fzdiffz0  10515  elfzo  10534  fzodcel  10538  elfzonlteqm1  10606  modqaddmulmod  10806  expdivap  11005  leexp2a  11007  bcval3  11167  omgadd  11220  ccatval1  11343  ccatval2  11344  ccatval3  11345  ccatass  11354  ccats1val2  11386  swrdval2  11401  swrdlen  11402  pfxfv  11434  pfxnd  11439  pfxsuffeqwrdeq  11448  swrdswrdlem  11454  swrdswrd  11455  pfxswrd  11456  pfxpfx  11458  ccats1pfxeq  11464  ccats1pfxeqrex  11465  pfxccatin12lem2  11481  pfxccatpfx1  11486  swrdccat3b  11490  pfxccatid  11491  shftfibg  11563  elicc4abs  11838  xrmaxltsup  12002  xrmaxadd  12005  xrlemininf  12015  xrminltinf  12016  mulcn2  12056  fsumsplitsnun  12164  prodfrecap  12291  demoivreALT  12519  dvdsval2  12535  dvdsmodexp  12540  dvdsmulcr  12566  modmulconst  12568  dvdsexp  12606  oddge22np1  12626  modremain  12674  mulgcd  12771  mulgcdr  12773  gcddiv  12774  rpmulgcd  12781  rplpwr  12782  coprmdvds  12848  cncongr1  12859  dvdsnprmd  12881  prmexpb  12907  rpexp  12909  cncongrprm  12913  modprm0  13011  modprmn0modprm0  13013  coprimeprodsq  13014  pythagtriplem1  13022  pythagtriplem3  13024  pythagtriplem10  13026  pythagtriplem6  13027  pythagtriplem11  13031  pythagtriplem12  13032  pythagtriplem13  13033  pythagtriplem15  13035  pythagtriplem17  13037  pythagtriplem19  13039  pcdvdsb  13077  dvdsprmpweqle  13094  pcfaclem  13106  ballotfilemieq  13238  ballotfilemrv1  13242  isstructr  13345  setsvala  13361  setsresg  13368  strle3g  13439  imasaddvallemg  13613  fvprif  13641  mgmsscl  13658  insubm  13769  dfgrp3mlem  13880  mulgdirlem  13933  mulgp1  13935  mulgmodid  13941  eqglact  14005  gsumconstcmn  14143  rngdi  14214  rngdir  14215  rmodislmodlem  14659  rmodislmod  14660  lssclg  14673  2idlcpblrng  14832  qusmulrng  14841  psrbagaddclfi  14984  clsss  15142  ntrcls0  15155  neiss  15174  neipsm  15178  cnpnei  15243  cncnp2m  15255  cnconst2  15257  sslm  15271  upxp  15296  txmetcn  15543  ptolemy  15848  sincosq1eq  15863  rplogbval  15970  rpcxplogb  15989  pellexlem1  16005  lgsdirprm  16067  lgsdirnn0  16080  gausslemma2dlem1a  16091  gausslemma2dlem3  16096  2lgslem1a1  16119  2lgsoddprmlem1  16138  2lgsoddprmlem2  16139  structiedg0val  16195  lpvtx  16234  incistruhgr  16245  upgredg2vtx  16303  upgredgpr  16304  ausgrumgrien  16325  ausgrusgrien  16326  ushgredgedg  16381  ushgredgedgloop  16383  uhgrissubgr  16416  egrsubgr  16418  0uhgrsubgr  16420  wlkvtxeledgg  16499  wlkeq  16509  wlkl1loop  16513  uspgr2wlkeq  16520  uspgr2wlkeq2  16521  wlkres  16534  loopclwwlkn1b  16574  clwwlkext2edg  16577  clwwlknonex2lem2  16593  clwwlknonex2  16594  clwwlknun  16596  eupth2lem3lem6fi  16626  findset  16885