Theorem 3ad2ant2 1050

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 1046	1 |- ( ( ps /\ ph /\ th ) -> 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:  simp2l  1054  simp2r  1055  simp21  1061  simp22  1062  simp23  1063  simp2ll  1095  simp2lr  1096  simp2rl  1097  simp2rr  1098  simp2l1  1127  simp2l2  1128  simp2l3  1129  simp2r1  1130  simp2r2  1131  simp2r3  1132  simp21l  1145  simp21r  1146  simp22l  1147  simp22r  1148  simp23l  1149  simp23r  1150  simp211  1166  simp212  1167  simp213  1168  simp221  1169  simp222  1170  simp223  1171  simp231  1172  simp232  1173  simp233  1174  3anim123i  1215  3jaao  1349  ceqsalt  2848  vtoclgft  2873  vtoclegft  2897  ifbothdc  3672  ifnebibdc  3683  frirrg  4490  elirr  4683  en2lp  4696  reg3exmidlemwe  4721  sotri3  5181  funtpg  5427  fnprg  5431  fntpg  5432  funimaexglem  5459  fnco  5486  fresaunres2disj  5565  fvun1  5763  oprssov  6221  caovimo  6273  suppsnopdc  6480  funsssuppss  6488  rdgivallem  6642  fnsnsplitdc  6768  funresdfunsndc  6769  mapsnd  6960  f1dom2g  7032  mapxpen  7138  ssfidc  7235  sbthlemi4  7267  ordiso2  7365  updjud  7412  difinfsn  7430  mkvprop  7488  endjudisj  7556  distrnqg  7744  distrnq0  7816  prarloclem5  7857  cauappcvgprlemlol  8004  cauappcvgprlemupu  8006  caucvgprlemlol  8027  caucvgprlemupu  8029  caucvgprprlemlol  8055  caucvgprprlemupu  8057  cnegexlem2  8492  apcotr  8925  apadd1  8926  mulext1  8930  div2negap  9055  ltdiv2  9207  nndivtr  9325  difgtsumgt  9693  zdivmul  9715  gtndiv  9720  fzind  9740  eluzuzle  9909  eluzp1p1  9927  peano2uz  9962  qdivcl  10022  irrmul  10026  ledivge1le  10106  xrre2  10202  xaddass  10250  xltadd1  10257  xlt2add  10261  ubioc1  10310  ubicc2  10366  zltaddlt1le  10389  uzsubsubfz  10430  elfz1b  10475  fzp1nel  10489  fz0fzdiffz0  10515  difelfzle  10519  elfzo0  10571  elfzonlteqm1  10606  fzonn0p1p1  10609  fzosplitprm1  10631  fzoshftral  10635  subfzo0  10639  ceiqle  10728  modqval  10739  modqvalr  10740  flqpmodeq  10742  modq0  10744  mulqmod0  10745  negqmod0  10746  modqge0  10747  modqlt  10748  modqelico  10749  modqdiffl  10750  modqmulnn  10757  modqvalp1  10758  modqmuladdnn0  10783  qnegmod  10784  addmodid  10787  q2submod  10800  modifeq2int  10801  modfzo0difsn  10810  addmodlteq  10813  mulsubdivbinom2ap  11127  omgadd  11220  hashun  11223  ccatass  11354  lswccatn0lsw  11357  ccats1val2  11386  swrd00g  11399  swrdval2  11401  swrdlen  11402  swrdfv  11403  swrdfv0  11404  swrdnd  11409  swrdlen2  11412  swrdfv2  11413  swrdsbslen  11416  swrdspsleq  11417  ccatswrd  11420  pfxfv  11434  pfxn0  11438  pfxnd  11439  pfxsuff1eqwrdeq  11449  pfxpfx  11458  ccats1pfxeq  11464  ccatopth2  11467  wrd2ind  11473  pfxccatin12lem3  11482  pfxccat3  11484  swrdccat  11485  pfxccat3a  11488  redivap  11617  imdivap  11624  xrmaxltsup  12002  xrmaxadd  12005  xrlemininf  12015  xrminltinf  12016  climuni  12037  mulcn2  12056  fsumsplitsnun  12164  prodfap0  12290  fprodabs  12361  efsub  12426  cos12dec  12513  dvdsmodexp  12540  summodnegmod  12567  divalglemex  12667  divalg  12669  modremain  12674  ndvdssub  12675  fldivndvdslt  12682  bitsfzo  12700  nndvdslegcd  12720  dfgcd2  12769  mulgcd  12771  mulgcdr  12773  gcddiv  12774  rplpwr  12782  rppwr  12783  qredeq  12852  divgcdcoprmex  12858  cncongr1  12859  cncongr2  12860  pw2dvdslemn  12921  hashgcdlem  12994  modprm0  13011  modprmn0modprm0  13013  pythagtriplem1  13022  pythagtriplem3  13024  pythagtriplem10  13026  pythagtriplem6  13027  pythagtriplem7  13028  pythagtriplem11  13031  pythagtriplem12  13032  pythagtriplem13  13033  pythagtriplem14  13034  pythagtriplem19  13039  pythagtrip  13040  dvdsprmpweqnn  13093  difsqpwdvds  13095  pcfaclem  13106  pcbc  13108  ballotfilemsgt1  13232  ballotfilemieq  13238  ballotfilemfrcn0  13251  unennn  13266  ptex  13595  imasaddvallemg  13613  fvprif  13641  mgmsscl  13658  insubm  13769  mulginvcom  13927  mulgassr  13940  mulgmodid  13941  quselbasg  14010  ghmnsgima  14048  gsumsncmn  14133  ringrng  14314  rmodislmodlem  14659  rmodislmod  14660  lssincl  14694  sralmod  14759  rnglidlmmgm  14805  rnglidlmsgrp  14806  rnglidlrng  14807  2idlcpblrng  14832  psrbaglesuppg  14980  psrbagaddclfi  14984  ntrin  15148  elnei  15176  restco  15198  cnpnei  15243  cncnp2m  15255  sslm  15271  upxp  15296  blres  15458  metcnp3  15535  tgqioo  15579  dvply1  15789  ptolemy  15848  cxpcom  15963  logbgcd1irr  15992  logbprmirr  15997  pellexlem1  16005  lgslem1  16033  lgsneg  16057  lgsdilem  16060  lgsdir  16068  lgssq2  16074  lgsdirnn0  16080  gausslemma2dlem1a  16091  2lgslem1a1  16119  incistruhgr  16245  upgrex  16258  uhgr2edg  16361  usgr2v1e2w  16401  issubgr2  16413  0uhgrsubgr  16420  subgrfun  16422  subgreldmiedg  16424  subumgredg2en  16426  iedginwlk  16512  uspgr2wlkeq2  16521  umgrclwwlkge2  16557  clwwlkext2edg  16577  clwwlknccat  16578  umgr2cwwk2dif  16579  umgr2cwwkdifex  16580  clwwlknonex2  16594