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  4470  elirr  4690  en2lp  4703  reg3exmidlemwe  4728  sotri2  5188  poltletr  5191  funprg  5434  funtpg  5435  fntpg  5440  funimaexglem  5467  fvun1  5772  ftpg  5902  fsnunf  5918  fsnunfv  5919  caovimo  6286  funsssuppss  6502  brtposg  6529  smoel  6575  rdgivallem  6656  frecsuclem  6681  domssr  7068  mapxpen  7152  unsnfi  7230  unsnfidcex  7231  unsnfidcel  7232  sbthlemi4  7282  elfir  7312  updjud  7428  ltsopi  7693  distrnqg  7760  ltmnqg  7774  mulcanenq0ec  7818  distrnq0  7832  prarloclem5  7873  1idprl  7963  1idpru  7964  ltaprg  7992  recexprlemopl  7998  recexprlemopu  8000  recexprlem1ssl  8006  aptipr  8014  ltmprr  8015  cauappcvgprlemlol  8020  cauappcvgprlemupu  8022  caucvgprlemlol  8043  caucvgprlemupu  8045  caucvgprprlemlol  8071  caucvgprprlemupu  8073  readdcan  8473  cnegexlem2  8509  addcan2  8514  ltadd2  8754  apreap  8923  ltmul1  8928  apcotr  8943  apadd1  8944  mulext1  8948  divdirap  9035  divcanap5  9052  ltdiv1  9206  ind1  9309  ind0  9310  lt2halves  9552  zdivmul  9747  eluzsub  9968  ledivge1le  10144  addlelt  10186  xaddass  10288  xleadd1  10294  xltadd1  10295  elioo5  10352  iccsupr  10385  iccneg  10408  icoshft  10409  icoshftf1o  10410  zltaddlt1le  10427  fzen  10464  elfz1b  10514  fzrevral  10529  fzshftral  10532  elfz0ubfz0  10549  elfz0fzfz0  10550  fz0fzelfz0  10551  fz0fzdiffz0  10554  elfzo  10573  fzodcel  10577  elfzonlteqm1  10645  modqaddmulmod  10849  expdivap  11048  leexp2a  11050  bcval3  11211  omgadd  11264  ccatval1  11387  ccatval2  11388  ccatval3  11389  ccatass  11398  ccats1val2  11430  swrdval2  11445  swrdlen  11446  pfxfv  11478  pfxnd  11483  pfxsuffeqwrdeq  11492  swrdswrdlem  11498  swrdswrd  11499  pfxswrd  11500  pfxpfx  11502  ccats1pfxeq  11508  ccats1pfxeqrex  11509  pfxccatin12lem2  11525  pfxccatpfx1  11530  swrdccat3b  11534  pfxccatid  11535  shftfibg  11607  elicc4abs  11883  xrmaxltsup  12049  xrmaxadd  12052  xrlemininf  12062  xrminltinf  12063  mulcn2  12103  fsumsplitsnun  12211  prodfrecap  12338  demoivreALT  12566  dvdsval2  12582  dvdsmodexp  12587  dvdsmulcr  12613  modmulconst  12615  dvdsexp  12653  oddge22np1  12673  modremain  12721  mulgcd  12818  mulgcdr  12820  gcddiv  12821  rpmulgcd  12828  rplpwr  12829  coprmdvds  12895  cncongr1  12906  dvdsnprmd  12928  prmexpb  12955  rpexp  12957  cncongrprm  12961  modprm0  13062  modprmn0modprm0  13064  coprimeprodsq  13065  pythagtriplem1  13073  pythagtriplem3  13075  pythagtriplem10  13077  pythagtriplem6  13078  pythagtriplem11  13082  pythagtriplem12  13083  pythagtriplem13  13084  pythagtriplem15  13086  pythagtriplem17  13088  pythagtriplem19  13090  pcdvdsb  13128  dvdsprmpweqle  13145  pcfaclem  13157  ballotfilemieq  13318  ballotfilemrv1  13322  isstructr  13425  setsvala  13441  setsresg  13448  strle3g  13521  imasaddvallemg  13695  fvprif  13723  mgmsscl  13740  insubm  13851  dfgrp3mlem  13962  mulgdirlem  14015  mulgp1  14017  mulgmodid  14023  eqglact  14087  gsumconstcmn  14266  rngdi  14346  rngdir  14347  rmodislmodlem  14796  rmodislmod  14797  lssclg  14810  2idlcpblrng  14969  qusmulrng  14978  assa2ass  15118  assa2ass2  15119  psrbagaddclfi  15170  clsss  15344  ntrcls0  15357  neiss  15376  neipsm  15380  cnpnei  15445  cncnp2m  15457  cnconst2  15459  sslm  15473  upxp  15498  txmetcn  15745  ptolemy  16051  sincosq1eq  16066  rplogbval  16181  rpcxplogb  16200  pellexlem1  16229  bcmono  16304  lgsdirprm  16358  lgsdirnn0  16371  gausslemma2dlem1a  16382  gausslemma2dlem3  16387  2lgslem1a1  16410  2lgsoddprmlem1  16429  2lgsoddprmlem2  16430  structiedg0val  16486  lpvtx  16525  incistruhgr  16536  upgredg2vtx  16594  upgredgpr  16595  ausgrumgrien  16616  ausgrusgrien  16617  ushgredgedg  16672  ushgredgedgloop  16674  uhgrissubgr  16707  egrsubgr  16709  0uhgrsubgr  16711  wlkvtxeledgg  16790  wlkeq  16800  wlkl1loop  16804  uspgr2wlkeq  16811  uspgr2wlkeq2  16812  wlkres  16825  loopclwwlkn1b  16865  clwwlkext2edg  16868  clwwlknonex2lem2  16884  clwwlknonex2  16885  clwwlknun  16887  eupth2lem3lem6fi  16917  findset  17176