Theorem 3ad2ant2 1045

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 1041	1 |- ( ( ps /\ ph /\ th ) -> 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:  simp2l  1049  simp2r  1050  simp21  1056  simp22  1057  simp23  1058  simp2ll  1090  simp2lr  1091  simp2rl  1092  simp2rr  1093  simp2l1  1122  simp2l2  1123  simp2l3  1124  simp2r1  1125  simp2r2  1126  simp2r3  1127  simp21l  1140  simp21r  1141  simp22l  1142  simp22r  1143  simp23l  1144  simp23r  1145  simp211  1161  simp212  1162  simp213  1163  simp221  1164  simp222  1165  simp223  1166  simp231  1167  simp232  1168  simp233  1169  3anim123i  1210  3jaao  1344  ceqsalt  2829  vtoclgft  2854  vtoclegft  2878  ifbothdc  3640  ifnebibdc  3651  frirrg  4447  elirr  4639  en2lp  4652  reg3exmidlemwe  4677  sotri3  5135  funtpg  5381  fnprg  5385  fntpg  5386  funimaexglem  5413  fnco  5440  fvun1  5712  oprssov  6164  caovimo  6216  rdgivallem  6547  fnsnsplitdc  6673  funresdfunsndc  6674  f1dom2g  6929  mapxpen  7034  ssfidc  7130  sbthlemi4  7159  ordiso2  7234  updjud  7281  difinfsn  7299  mkvprop  7357  endjudisj  7425  distrnqg  7607  distrnq0  7679  prarloclem5  7720  cauappcvgprlemlol  7867  cauappcvgprlemupu  7869  caucvgprlemlol  7890  caucvgprlemupu  7892  caucvgprprlemlol  7918  caucvgprprlemupu  7920  cnegexlem2  8355  apcotr  8787  apadd1  8788  mulext1  8792  div2negap  8915  ltdiv2  9067  nndivtr  9185  difgtsumgt  9549  zdivmul  9570  gtndiv  9575  fzind  9595  eluzuzle  9764  eluzp1p1  9782  peano2uz  9817  qdivcl  9877  irrmul  9881  ledivge1le  9961  xrre2  10056  xaddass  10104  xltadd1  10111  xlt2add  10115  ubioc1  10164  ubicc2  10220  zltaddlt1le  10242  uzsubsubfz  10282  elfz1b  10325  fzp1nel  10339  fz0fzdiffz0  10365  difelfzle  10369  elfzo0  10421  elfzonlteqm1  10456  fzonn0p1p1  10459  fzosplitprm1  10481  fzoshftral  10485  subfzo0  10489  ceiqle  10576  modqval  10587  modqvalr  10588  flqpmodeq  10590  modq0  10592  mulqmod0  10593  negqmod0  10594  modqge0  10595  modqlt  10596  modqelico  10597  modqdiffl  10598  modqmulnn  10605  modqvalp1  10606  modqmuladdnn0  10631  qnegmod  10632  addmodid  10635  q2submod  10648  modifeq2int  10649  modfzo0difsn  10658  addmodlteq  10661  mulsubdivbinom2ap  10974  omgadd  11066  hashun  11069  ccatass  11189  lswccatn0lsw  11192  ccats1val2  11221  swrd00g  11234  swrdval2  11236  swrdlen  11237  swrdfv  11238  swrdfv0  11239  swrdnd  11244  swrdlen2  11247  swrdfv2  11248  swrdsbslen  11251  swrdspsleq  11252  ccatswrd  11255  pfxfv  11269  pfxn0  11273  pfxnd  11274  pfxsuff1eqwrdeq  11284  pfxpfx  11293  ccats1pfxeq  11299  ccatopth2  11302  wrd2ind  11308  pfxccatin12lem3  11317  pfxccat3  11319  swrdccat  11320  pfxccat3a  11323  redivap  11452  imdivap  11459  xrmaxltsup  11836  xrmaxadd  11839  xrlemininf  11849  xrminltinf  11850  climuni  11871  mulcn2  11890  fsumsplitsnun  11998  prodfap0  12124  fprodabs  12195  efsub  12260  cos12dec  12347  dvdsmodexp  12374  summodnegmod  12401  divalglemex  12501  divalg  12503  modremain  12508  ndvdssub  12509  fldivndvdslt  12516  bitsfzo  12534  nndvdslegcd  12554  dfgcd2  12603  mulgcd  12605  mulgcdr  12607  gcddiv  12608  rplpwr  12616  rppwr  12617  qredeq  12686  divgcdcoprmex  12692  cncongr1  12693  cncongr2  12694  pw2dvdslemn  12755  hashgcdlem  12828  modprm0  12845  modprmn0modprm0  12847  pythagtriplem1  12856  pythagtriplem3  12858  pythagtriplem10  12860  pythagtriplem6  12861  pythagtriplem7  12862  pythagtriplem11  12865  pythagtriplem12  12866  pythagtriplem13  12867  pythagtriplem14  12868  pythagtriplem19  12873  pythagtrip  12874  dvdsprmpweqnn  12927  difsqpwdvds  12929  pcfaclem  12940  pcbc  12942  unennn  13036  ptex  13365  imasaddvallemg  13416  fvprif  13444  mgmsscl  13462  insubm  13586  mulginvcom  13752  mulgassr  13765  mulgmodid  13766  quselbasg  13835  ghmnsgima  13873  ringrng  14068  rmodislmodlem  14383  rmodislmod  14384  lssincl  14418  sralmod  14483  rnglidlmmgm  14529  rnglidlmsgrp  14530  rnglidlrng  14531  2idlcpblrng  14556  psrbaglesuppg  14705  ntrin  14867  elnei  14895  restco  14917  cnpnei  14962  cncnp2m  14974  sslm  14990  upxp  15015  blres  15177  metcnp3  15254  tgqioo  15298  dvply1  15508  ptolemy  15567  cxpcom  15681  logbgcd1irr  15710  logbprmirr  15715  lgslem1  15748  lgsneg  15772  lgsdilem  15775  lgsdir  15783  lgssq2  15789  lgsdirnn0  15795  gausslemma2dlem1a  15806  2lgslem1a1  15834  incistruhgr  15960  upgrex  15973  uhgr2edg  16076  usgr2v1e2w  16116  issubgr2  16128  0uhgrsubgr  16135  subgrfun  16137  subgreldmiedg  16139  subumgredg2en  16141  iedginwlk  16227  uspgr2wlkeq2  16236  umgrclwwlkge2  16272  clwwlkext2edg  16292  clwwlknccat  16293  umgr2cwwk2dif  16294  umgr2cwwkdifex  16295  clwwlknonex2  16309  gfsumsn  16737