Theorem 3ad2ant1 1020

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

Hypothesis

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

Assertion

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

Proof of Theorem 3ad2ant1

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

Syntax hints:   -> wi 4   /\ w3a 980

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 982

This theorem is referenced by:  simp1l  1023  simp1r  1024  simp11  1029  simp12  1030  simp13  1031  simp1ll  1062  simp1lr  1063  simp1rl  1064  simp1rr  1065  simp1l1  1092  simp1l2  1093  simp1l3  1094  simp1r1  1095  simp1r2  1096  simp1r3  1097  simp11l  1110  simp11r  1111  simp12l  1112  simp12r  1113  simp13l  1114  simp13r  1115  simp111  1128  simp112  1129  simp113  1130  simp121  1131  simp122  1132  simp123  1133  simp131  1134  simp132  1135  simp133  1136  3anim123i  1186  3jaao  1319  ceqsalt  2786  sbciegft  3016  reupick2  3445  ifbothdc  3590  frirrg  4381  breldmg  4868  fntpg  5310  funimaexglem  5337  fex2  5422  fvun1  5623  fprg  5741  fsnunfv  5759  fnfvima  5793  cocan1  5830  cocan2  5831  mpoeq3dv  5984  fovcld  6023  funexw  6164  mpofvex  6256  poxp  6285  smoiso  6355  tfrlem5  6367  tfrlemibxssdm  6380  tfr1onlembfn  6397  tfri1dALT  6404  tfrcllembfn  6410  rdgon  6439  freccllem  6455  nnawordex  6582  mapxpen  6904  fidceq  6925  fidifsnen  6926  dif1en  6935  en2eqpr  6963  unsnfi  6975  unsnfidcex  6976  unsnfidcel  6977  fisseneq  6988  ordiso2  7094  updjud  7141  mkvprop  7217  endjudisj  7270  xpdjuen  7278  mulcanenq0ec  7505  prltlu  7547  prarloclem3step  7556  prarloclem5  7560  ltasrg  7830  cnegexlem1  8194  addcan  8199  apcotr  8626  apadd1  8627  mulext1  8631  divdivap1  8742  divdivap2  8743  div2negap  8754  divneg2ap  8755  ltmulgt11  8883  ltdiv2  8906  squeeze0  8923  nndivtr  9024  nn0n0n1ge2  9387  zdivmul  9407  gtndiv  9412  eluzuzle  9600  eluzp1p1  9618  qdivcl  9708  irrmul  9712  rpgecl  9748  xaddass  9935  xltadd1  9942  xlt2add  9946  lbico1  9996  lbicc2  10050  zltaddlt1le  10073  uzsubsubfz  10113  elfz1b  10156  elfz0ubfz0  10191  fz0fzelfz0  10193  difelfzle  10200  difelfznle  10201  2ffzeq  10207  fzo1fzo0n0  10250  ubmelfzo  10267  fzonn0p1p1  10280  elfzom1p1elfzo  10281  elfzonelfzo  10297  subfzo0  10309  ceiqle  10384  ceilqle  10385  modqval  10395  flqpmodeq  10398  modq0  10400  negqmod0  10402  modqge0  10403  modqlt  10404  modqdiffl  10406  modqmulnn  10413  modqvalp1  10414  modqmuladdnn0  10439  qnegmod  10440  addmodid  10443  modfzo0difsn  10466  addmodlteq  10469  qexpclz  10631  expgt1  10648  expp1zap  10659  expm1ap  10660  expubnd  10667  bernneq2  10732  expnlbnd  10735  mulsubdivbinom2ap  10782  omgadd  10873  hashun  10876  fihashssdif  10889  hashdifpr  10891  fimaxq  10898  shftuz  10961  mulreap  11008  redivap  11018  imdivap  11025  resqrtcl  11173  xrmaxltsup  11401  xrmaxaddlem  11403  xrmaxadd  11404  xrlemininf  11414  xrminltinf  11415  climuni  11436  addcn2  11453  mulcn2  11455  efsub  11824  sin02gt0  11907  cos12dec  11911  dvdsval2  11933  addmodlteqALT  12001  modremain  12070  fldivndvdslt  12076  mulgcdr  12155  gcddiv  12156  rpmulgcd  12163  rplpwr  12164  rppwr  12165  nnminle  12172  qredeq  12234  divgcdcoprmex  12240  cncongr1  12241  cncongr2  12242  dvdsnprmd  12263  euclemma  12284  prmexpb  12289  qnumdenbi  12330  eulerth  12371  fermltl  12372  prmdiv  12373  hashgcdlem  12376  odzcllem  12380  vfermltl  12389  reumodprminv  12391  modprm0  12392  modprmn0modprm0  12394  coprimeprodsq  12395  pythagtriplem1  12403  pythagtriplem3  12405  pythagtriplem4  12406  pythagtriplem10  12407  pythagtriplem6  12408  pythagtriplem7  12409  pythagtriplem8  12410  pythagtriplem9  12411  pythagtriplem11  12412  pythagtriplem12  12413  pythagtriplem13  12414  pythagtriplem14  12415  pythagtriplem15  12416  pythagtriplem16  12417  pythagtriplem17  12418  pythagtriplem19  12420  pythagtrip  12421  pcpremul  12431  pcdvdsb  12458  dvdsprmpweqnn  12474  dvdsprmpweqle  12475  difsqpwdvds  12476  pcfaclem  12487  pcbc  12489  4sqlem12  12540  unennn  12554  nninfdc  12610  setsex  12650  f1ocpbllem  12893  imasaddfnlemg  12897  imasaddvallemg  12898  ercpbl  12914  erlecpbl  12915  qusaddvallemg  12916  fvprif  12926  xpsfrnel2  12929  plusfvalg  12946  insubm  13057  grpidrcan  13137  grpidlcan  13138  grpsubpropd2  13177  imasgrp2  13180  imasgrp  13181  mulgnnsubcl  13204  mulgnn0subcl  13205  mulgsubcl  13206  mulgaddcom  13216  mulginvcom  13217  mulgnnass  13227  mulgassr  13230  mulgpropdg  13234  submmulg  13236  subgcl  13254  subgsubcl  13255  subgsub  13256  subgmulg  13258  nsgconj  13276  ghmsub  13321  ghmrn  13327  ghmeqker  13341  f1ghm0to0  13342  ablinvadd  13380  ablsub4  13383  abladdsub4  13384  subcmnd  13403  imasabl  13406  rngcl  13440  imasrng  13452  srgcl  13466  srg1zr  13483  srgen1zr  13484  ringcl  13509  crngcom  13510  ringidss  13525  mulgass2  13554  imasring  13560  opprmulg  13567  unitmulclb  13610  unitdvcl  13632  rhmmul  13660  rhmdvdsr  13671  subrngmcl  13705  subrgmcl  13729  subrgdv  13734  subrgugrp  13736  domneq0  13768  scafvalg  13803  lmodprop2d  13844  lssclg  13860  lssvnegcl  13872  lssintclm  13880  sralmod  13946  rnglidlmcl  13976  lidlnegcl  13981  rspssp  13990  rnglidlmsgrp  13993  rnglidlrng  13994  2idlcpblrng  14019  qus2idrng  14021  zndvds  14137  znleval2  14142  basgen  14248  2basgeng  14250  iuncld  14283  neipsm  14322  opnneissb  14323  opnssneib  14324  iscnp3  14371  cnprcl2k  14374  cnpnei  14387  cncnp2m  14399  cnptoprest  14407  sslm  14415  upxp  14440  cnmpt22  14462  distspace  14503  0met  14552  blvalps  14556  blval  14557  ssblps  14593  ssbl  14594  blpnfctr  14607  blopn  14658  blnei  14660  bdxmet  14669  bdbl  14671  metcnp3  14679  tgqioo  14715  ptolemy  14959  sinq12gt0  14965  sincosq1eq  14974  rpcxpadd  15040  cxpmul  15047  rplogbval  15077  logbleb  15093  logbgcd1irr  15099  logbprmirr  15104  lgsfvalg  15121  lgsneg1  15141  lgssq  15156  lgsdinn0  15164  gausslemma2dlem1a  15174  2lgsoddprmlem2  15194  bdfind  15438  1dom1el  15483