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  7423  ltsopi  7688  distrnqg  7755  ltmnqg  7769  mulcanenq0ec  7813  distrnq0  7827  prarloclem5  7868  1idprl  7958  1idpru  7959  ltaprg  7987  recexprlemopl  7993  recexprlemopu  7995  recexprlem1ssl  8001  aptipr  8009  ltmprr  8010  cauappcvgprlemlol  8015  cauappcvgprlemupu  8017  caucvgprlemlol  8038  caucvgprlemupu  8040  caucvgprprlemlol  8066  caucvgprprlemupu  8068  readdcan  8468  cnegexlem2  8504  addcan2  8509  ltadd2  8749  apreap  8918  ltmul1  8923  apcotr  8938  apadd1  8939  mulext1  8943  divdirap  9030  divcanap5  9047  ltdiv1  9201  ind1  9303  ind0  9304  lt2halves  9546  zdivmul  9741  eluzsub  9962  ledivge1le  10138  addlelt  10180  xaddass  10282  xleadd1  10288  xltadd1  10289  elioo5  10346  iccsupr  10379  iccneg  10402  icoshft  10403  icoshftf1o  10404  zltaddlt1le  10421  fzen  10458  elfz1b  10508  fzrevral  10523  fzshftral  10526  elfz0ubfz0  10543  elfz0fzfz0  10544  fz0fzelfz0  10545  fz0fzdiffz0  10548  elfzo  10567  fzodcel  10571  elfzonlteqm1  10639  modqaddmulmod  10843  expdivap  11042  leexp2a  11044  bcval3  11205  omgadd  11258  ccatval1  11381  ccatval2  11382  ccatval3  11383  ccatass  11392  ccats1val2  11424  swrdval2  11439  swrdlen  11440  pfxfv  11472  pfxnd  11477  pfxsuffeqwrdeq  11486  swrdswrdlem  11492  swrdswrd  11493  pfxswrd  11494  pfxpfx  11496  ccats1pfxeq  11502  ccats1pfxeqrex  11503  pfxccatin12lem2  11519  pfxccatpfx1  11524  swrdccat3b  11528  pfxccatid  11529  shftfibg  11601  elicc4abs  11877  xrmaxltsup  12043  xrmaxadd  12046  xrlemininf  12056  xrminltinf  12057  mulcn2  12097  fsumsplitsnun  12205  prodfrecap  12332  demoivreALT  12560  dvdsval2  12576  dvdsmodexp  12581  dvdsmulcr  12607  modmulconst  12609  dvdsexp  12647  oddge22np1  12667  modremain  12715  mulgcd  12812  mulgcdr  12814  gcddiv  12815  rpmulgcd  12822  rplpwr  12823  coprmdvds  12889  cncongr1  12900  dvdsnprmd  12922  prmexpb  12949  rpexp  12951  cncongrprm  12955  modprm0  13056  modprmn0modprm0  13058  coprimeprodsq  13059  pythagtriplem1  13067  pythagtriplem3  13069  pythagtriplem10  13071  pythagtriplem6  13072  pythagtriplem11  13076  pythagtriplem12  13077  pythagtriplem13  13078  pythagtriplem15  13080  pythagtriplem17  13082  pythagtriplem19  13084  pcdvdsb  13122  dvdsprmpweqle  13139  pcfaclem  13151  ballotfilemieq  13312  ballotfilemrv1  13316  isstructr  13419  setsvala  13435  setsresg  13442  strle3g  13515  imasaddvallemg  13689  fvprif  13717  mgmsscl  13734  insubm  13845  dfgrp3mlem  13956  mulgdirlem  14009  mulgp1  14011  mulgmodid  14017  eqglact  14081  gsumconstcmn  14250  rngdi  14323  rngdir  14324  rmodislmodlem  14771  rmodislmod  14772  lssclg  14785  2idlcpblrng  14944  qusmulrng  14953  assa2ass  15093  assa2ass2  15094  psrbagaddclfi  15145  clsss  15310  ntrcls0  15323  neiss  15342  neipsm  15346  cnpnei  15411  cncnp2m  15423  cnconst2  15425  sslm  15439  upxp  15464  txmetcn  15711  ptolemy  16017  sincosq1eq  16032  rplogbval  16142  rpcxplogb  16161  pellexlem1  16190  bcmono  16265  lgsdirprm  16319  lgsdirnn0  16332  gausslemma2dlem1a  16343  gausslemma2dlem3  16348  2lgslem1a1  16371  2lgsoddprmlem1  16390  2lgsoddprmlem2  16391  structiedg0val  16447  lpvtx  16486  incistruhgr  16497  upgredg2vtx  16555  upgredgpr  16556  ausgrumgrien  16577  ausgrusgrien  16578  ushgredgedg  16633  ushgredgedgloop  16635  uhgrissubgr  16668  egrsubgr  16670  0uhgrsubgr  16672  wlkvtxeledgg  16751  wlkeq  16761  wlkl1loop  16765  uspgr2wlkeq  16772  uspgr2wlkeq2  16773  wlkres  16786  loopclwwlkn1b  16826  clwwlkext2edg  16829  clwwlknonex2lem2  16845  clwwlknonex2  16846  clwwlknun  16848  eupth2lem3lem6fi  16878  findset  17137