Theorem 3ad2ant2 1046

Description: Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)

Hypothesis

Ref	Expression
3ad2ant.1	|- ( ph -> ch )

Assertion

Ref	Expression
3ad2ant2	|- ( ( ps /\ ph /\ th ) -> ch )

Proof of Theorem 3ad2ant2

Step	Hyp	Ref	Expression
1		3ad2ant.1	. . 3 |- ( ph -> ch )
2	1	adantr 276	. 2 |- ( ( ph /\ th ) -> ch )
3	2	3adant1 1042	1 |- ( ( ps /\ ph /\ th ) -> ch )

Syntax hints:   -> wi 4   /\ w3a 1005

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 1007

This theorem is referenced by:  simp2l  1050  simp2r  1051  simp21  1057  simp22  1058  simp23  1059  simp2ll  1091  simp2lr  1092  simp2rl  1093  simp2rr  1094  simp2l1  1123  simp2l2  1124  simp2l3  1125  simp2r1  1126  simp2r2  1127  simp2r3  1128  simp21l  1141  simp21r  1142  simp22l  1143  simp22r  1144  simp23l  1145  simp23r  1146  simp211  1162  simp212  1163  simp213  1164  simp221  1165  simp222  1166  simp223  1167  simp231  1168  simp232  1169  simp233  1170  3anim123i  1211  3jaao  1345  ceqsalt  2842  vtoclgft  2867  vtoclegft  2891  ifbothdc  3661  ifnebibdc  3672  frirrg  4476  elirr  4668  en2lp  4681  reg3exmidlemwe  4706  sotri3  5166  funtpg  5412  fnprg  5416  fntpg  5417  funimaexglem  5444  fnco  5471  fresaunres2disj  5550  fvun1  5748  oprssov  6204  caovimo  6256  suppsnopdc  6463  funsssuppss  6471  rdgivallem  6625  fnsnsplitdc  6751  funresdfunsndc  6752  mapsnd  6936  f1dom2g  7008  mapxpen  7114  ssfidc  7211  sbthlemi4  7243  ordiso2  7339  updjud  7386  difinfsn  7404  mkvprop  7462  endjudisj  7530  distrnqg  7718  distrnq0  7790  prarloclem5  7831  cauappcvgprlemlol  7978  cauappcvgprlemupu  7980  caucvgprlemlol  8001  caucvgprlemupu  8003  caucvgprprlemlol  8029  caucvgprprlemupu  8031  cnegexlem2  8465  apcotr  8898  apadd1  8899  mulext1  8903  div2negap  9026  ltdiv2  9178  nndivtr  9296  difgtsumgt  9664  zdivmul  9686  gtndiv  9691  fzind  9711  eluzuzle  9880  eluzp1p1  9898  peano2uz  9933  qdivcl  9993  irrmul  9997  ledivge1le  10077  xrre2  10173  xaddass  10221  xltadd1  10228  xlt2add  10232  ubioc1  10281  ubicc2  10337  zltaddlt1le  10360  uzsubsubfz  10401  elfz1b  10446  fzp1nel  10460  fz0fzdiffz0  10486  difelfzle  10490  elfzo0  10542  elfzonlteqm1  10577  fzonn0p1p1  10580  fzosplitprm1  10602  fzoshftral  10606  subfzo0  10610  ceiqle  10699  modqval  10710  modqvalr  10711  flqpmodeq  10713  modq0  10715  mulqmod0  10716  negqmod0  10717  modqge0  10718  modqlt  10719  modqelico  10720  modqdiffl  10721  modqmulnn  10728  modqvalp1  10729  modqmuladdnn0  10754  qnegmod  10755  addmodid  10758  q2submod  10771  modifeq2int  10772  modfzo0difsn  10781  addmodlteq  10784  mulsubdivbinom2ap  11098  omgadd  11191  hashun  11194  ccatass  11321  lswccatn0lsw  11324  ccats1val2  11353  swrd00g  11366  swrdval2  11368  swrdlen  11369  swrdfv  11370  swrdfv0  11371  swrdnd  11376  swrdlen2  11379  swrdfv2  11380  swrdsbslen  11383  swrdspsleq  11384  ccatswrd  11387  pfxfv  11401  pfxn0  11405  pfxnd  11406  pfxsuff1eqwrdeq  11416  pfxpfx  11425  ccats1pfxeq  11431  ccatopth2  11434  wrd2ind  11440  pfxccatin12lem3  11449  pfxccat3  11451  swrdccat  11452  pfxccat3a  11455  redivap  11584  imdivap  11591  xrmaxltsup  11968  xrmaxadd  11971  xrlemininf  11981  xrminltinf  11982  climuni  12003  mulcn2  12022  fsumsplitsnun  12130  prodfap0  12256  fprodabs  12327  efsub  12392  cos12dec  12479  dvdsmodexp  12506  summodnegmod  12533  divalglemex  12633  divalg  12635  modremain  12640  ndvdssub  12641  fldivndvdslt  12648  bitsfzo  12666  nndvdslegcd  12686  dfgcd2  12735  mulgcd  12737  mulgcdr  12739  gcddiv  12740  rplpwr  12748  rppwr  12749  qredeq  12818  divgcdcoprmex  12824  cncongr1  12825  cncongr2  12826  pw2dvdslemn  12887  hashgcdlem  12960  modprm0  12977  modprmn0modprm0  12979  pythagtriplem1  12988  pythagtriplem3  12990  pythagtriplem10  12992  pythagtriplem6  12993  pythagtriplem7  12994  pythagtriplem11  12997  pythagtriplem12  12998  pythagtriplem13  12999  pythagtriplem14  13000  pythagtriplem19  13005  pythagtrip  13006  dvdsprmpweqnn  13059  difsqpwdvds  13061  pcfaclem  13072  pcbc  13074  ballotfilemsgt1  13198  ballotfilemieq  13204  ballotfilemfrcn0  13217  unennn  13232  ptex  13561  imasaddvallemg  13579  fvprif  13607  mgmsscl  13624  insubm  13740  mulginvcom  13900  mulgassr  13913  mulgmodid  13914  quselbasg  13983  ghmnsgima  14021  gfsumsn  14107  ringrng  14279  rmodislmodlem  14624  rmodislmod  14625  lssincl  14659  sralmod  14724  rnglidlmmgm  14770  rnglidlmsgrp  14771  rnglidlrng  14772  2idlcpblrng  14797  psrbaglesuppg  14947  psrbagaddclfi  14951  ntrin  15115  elnei  15143  restco  15165  cnpnei  15210  cncnp2m  15222  sslm  15238  upxp  15263  blres  15425  metcnp3  15502  tgqioo  15546  dvply1  15756  ptolemy  15815  cxpcom  15929  logbgcd1irr  15958  logbprmirr  15963  pellexlem1  15971  lgslem1  15999  lgsneg  16023  lgsdilem  16026  lgsdir  16034  lgssq2  16040  lgsdirnn0  16046  gausslemma2dlem1a  16057  2lgslem1a1  16085  incistruhgr  16211  upgrex  16224  uhgr2edg  16327  usgr2v1e2w  16367  issubgr2  16379  0uhgrsubgr  16386  subgrfun  16388  subgreldmiedg  16390  subumgredg2en  16392  iedginwlk  16478  uspgr2wlkeq2  16487  umgrclwwlkge2  16523  clwwlkext2edg  16543  clwwlknccat  16544  umgr2cwwk2dif  16545  umgr2cwwkdifex  16546  clwwlknonex2  16560