Theorem 3ad2ant1 1049

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 1047	1 |- ( ( ph /\ ps /\ th ) -> 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:  simp1l  1052  simp1r  1053  simp11  1058  simp12  1059  simp13  1060  simp1ll  1091  simp1lr  1092  simp1rl  1093  simp1rr  1094  simp1l1  1121  simp1l2  1122  simp1l3  1123  simp1r1  1124  simp1r2  1125  simp1r3  1126  simp11l  1139  simp11r  1140  simp12l  1141  simp12r  1142  simp13l  1143  simp13r  1144  simp111  1157  simp112  1158  simp113  1159  simp121  1160  simp122  1161  simp123  1162  simp131  1163  simp132  1164  simp133  1165  3anim123i  1215  3jaao  1349  ceqsalt  2848  sbciegft  3082  reupick2  3519  ifbothdc  3675  ifprdc  3819  frirrg  4497  breldmg  4989  fntpg  5440  funimaexglem  5467  fex2  5559  fresaunres2disj  5573  fvun1  5772  fprg  5901  fsnunfv  5919  fnfvima  5956  cocan1  5996  cocan2  5997  mpoeq3dv  6157  fovcld  6196  fvmpopr2d  6228  funexw  6345  mpofvex  6445  poxp  6472  suppval1  6483  suppvalfng  6484  suppvalfn  6485  suppimacnvfn  6490  suppsnopdc  6494  smoiso  6577  tfrlem5  6589  tfrlemibxssdm  6602  tfr1onlembfn  6619  tfri1dALT  6626  tfrcllembfn  6632  rdgon  6661  freccllem  6677  nnawordex  6806  1dom1el  7111  mapxpen  7152  fidceq  7175  fidifsnen  7176  dif1en  7187  en2eqpr  7218  unsnfi  7230  unsnfidcex  7231  unsnfidcel  7232  fisseneq  7246  funisfsupp  7296  ordiso2  7381  updjud  7428  mkvprop  7504  endjudisj  7572  xpdjuen  7580  mulcanenq0ec  7818  prltlu  7860  prarloclem3step  7869  prarloclem5  7873  ltasrg  8143  cnegexlem1  8508  addcan  8513  apcotr  8943  apadd1  8944  mulext1  8948  divdivap1  9061  divdivap2  9062  div2negap  9073  divneg2ap  9074  ltmulgt11  9202  ltdiv2  9225  squeeze0  9242  nndivtr  9355  nn0n0n1ge2  9726  zdivmul  9747  gtndiv  9752  eluzuzle  9946  eluzp1p1  9964  qdivcl  10059  irrmul  10064  rpgecl  10100  xaddass  10288  xltadd1  10295  xlt2add  10299  lbico1  10349  lbicc2  10403  zltaddlt1le  10427  uzsubsubfz  10469  elfz1b  10514  elfz0ubfz0  10549  fz0fzelfz0  10551  difelfzle  10558  difelfznle  10559  2ffzeq  10565  fzo1fzo0n0  10612  ubmelfzo  10635  fzonn0p1p1  10648  elfzom1p1elfzo  10649  elfzonelfzo  10665  subfzo0  10678  ceiqle  10771  ceilqle  10772  modqval  10782  flqpmodeq  10785  modq0  10787  negqmod0  10789  modqge0  10790  modqlt  10791  modqdiffl  10793  modqmulnn  10800  modqvalp1  10801  modqmuladdnn0  10826  qnegmod  10827  addmodid  10830  modfzo0difsn  10853  addmodlteq  10856  qexpclz  11018  expgt1  11035  expp1zap  11046  expm1ap  11047  expubnd  11054  bernneq2  11120  expnlbnd  11123  mulsubdivbinom2ap  11171  omgadd  11264  hashun  11267  fihashssdif  11281  hashdifpr  11283  fimaxq  11292  ccatval2  11388  ccatval3  11389  ccatval1lsw  11394  ccatval21sw  11395  ccatass  11398  ccatw2s1leng  11428  ccats1val2  11430  ccat2s1fvwd  11437  fzowrddc  11441  swrdval  11442  swrdclg  11444  swrdval2  11445  swrdnd  11453  swrdlen2  11456  swrdfv2  11457  ccatswrd  11464  pfxn0  11482  pfxsuff1eqwrdeq  11493  swrdswrdlem  11498  ccats1pfxeq  11508  ccats1pfxeqrex  11509  ccatopth2  11511  wrd2ind  11517  pfxccatin12lem3  11526  pfxccat3  11528  swrdccat  11529  pfxccatpfx2  11531  pfxccat3a  11532  swrdccat3b  11534  pfxccatid  11535  ccats1pfxeqbi  11536  shftuz  11604  mulreap  11651  redivap  11661  imdivap  11668  resqrtcl  11817  xrmaxltsup  12049  xrmaxaddlem  12051  xrmaxadd  12052  xrlemininf  12062  xrminltinf  12063  climuni  12084  addcn2  12101  mulcn2  12103  efsub  12473  sin02gt0  12556  cos12dec  12560  dvdsval2  12582  addmodlteqALT  12651  modremain  12721  fldivndvdslt  12729  mulgcdr  12820  gcddiv  12821  rpmulgcd  12828  rplpwr  12829  rppwr  12830  nnminle  12837  qredeq  12899  divgcdcoprmex  12905  cncongr1  12906  cncongr2  12907  dvdsnprmd  12928  euclemma  12950  prmexpb  12955  qnumdenbi  12997  eulerth  13040  fermltl  13041  prmdiv  13042  hashgcdlem  13045  odzcllem  13050  vfermltl  13059  reumodprminv  13061  modprm0  13062  modprmn0modprm0  13064  coprimeprodsq  13065  pythagtriplem1  13073  pythagtriplem3  13075  pythagtriplem4  13076  pythagtriplem10  13077  pythagtriplem6  13078  pythagtriplem7  13079  pythagtriplem8  13080  pythagtriplem9  13081  pythagtriplem11  13082  pythagtriplem12  13083  pythagtriplem13  13084  pythagtriplem14  13085  pythagtriplem15  13086  pythagtriplem16  13087  pythagtriplem17  13088  pythagtriplem19  13090  pythagtrip  13091  pcpremul  13101  pcdvdsb  13128  dvdsprmpweqnn  13144  dvdsprmpweqle  13145  difsqpwdvds  13146  pcfaclem  13157  pcbc  13159  4sqlem12  13210  ballotfilemsgt1  13312  ballotfilemieq  13318  ballotfilemfrcn0  13331  unennn  13346  nninfdc  13402  setsex  13442  f1ocpbllem  13690  imasaddfnlemg  13694  imasaddvallemg  13695  ercpbl  13711  erlecpbl  13712  qusaddvallemg  13713  fvprif  13723  xpsfrnel2  13726  plusfvalg  13742  imasmnd  13819  insubm  13851  grpidrcan  13929  grpidlcan  13930  grpsubpropd2  13969  imasgrp2  13972  imasgrp  13973  mulgnnsubcl  13996  mulgnn0subcl  13997  mulgsubcl  13998  mulgaddcom  14008  mulginvcom  14009  mulgnnass  14019  mulgassr  14022  mulgpropdg  14026  submmulg  14028  subgcl  14046  subgsubcl  14047  subgsub  14048  subgmulg  14050  nsgconj  14068  ghmsub  14113  ghmrn  14119  ghmeqker  14133  f1ghm0to0  14134  ablinvadd  14204  ablsub4  14207  abladdsub4  14208  subcmnd  14227  imasabl  14230  gsumconstcmn  14266  pwsinvg  14322  rngcl  14350  imasrng  14362  rng1zrlem  14365  rng1zr  14366  rngen1zr0  14368  srgcl  14381  srg1zr  14398  srgen1zr0  14399  ringcl  14424  crngcom  14425  ringidss  14441  mulgass2  14470  imasring  14478  opprmulg  14485  unitmulclb  14530  unitdvcl  14552  rhmmul  14580  rhmdvdsr  14591  subrngmcl  14626  subrgmcl  14650  subrgdv  14655  subrgugrp  14657  domneq0  14690  scafvalg  14753  lmodprop2d  14794  lssclg  14810  lssvnegcl  14822  lssintclm  14830  sralmod  14896  rnglidlmcl  14926  lidlnegcl  14931  rspssp  14940  rnglidlmsgrp  14943  rnglidlrng  14944  2idlcpblrng  14969  qus2idrng  14971  zndvds  15093  znleval2  15098  assa2ass  15118  assa2ass2  15119  asclmul1  15138  asclmul2  15139  ascldimul  15140  asclmulg  15153  psrbaglesupp  15167  psrbaglecl  15169  psrbagaddclfi  15170  psrbagcon  15171  psrringfi  15204  basgen  15306  2basgeng  15308  iuncld  15341  neipsm  15380  opnneissb  15381  opnssneib  15382  iscnp3  15429  cnprcl2k  15432  cnpnei  15445  cncnp2m  15457  cnptoprest  15465  sslm  15473  upxp  15498  cnmpt22  15520  distspace  15561  0met  15610  blvalps  15614  blval  15615  ssblps  15651  ssbl  15652  blpnfctr  15665  blopn  15716  blnei  15718  bdxmet  15727  bdbl  15729  metcnp3  15737  tgqioo  15781  ptolemy  16051  sinq12gt0  16057  sincosq1eq  16066  rpcxpadd  16138  cxpmul  16145  rplogbval  16181  logbleb  16197  logbgcd1irr  16203  logbprmirr  16208  pellexlem1  16229  chtqwordi  16263  efchtqdvds  16265  ppiqwordi  16268  bcmono  16304  lgsfvalg  16329  lgsneg1  16349  lgssq  16364  lgsdinn0  16372  gausslemma2dlem1a  16382  2lgs  16428  2lgsoddprmlem2  16430  funvtxdm2domval  16475  funiedgdm2domval  16476  iedgedgg  16507  lpvtx  16525  incistruhgr  16536  ausgrumgrien  16616  ausgrusgrien  16617  umgr2edgneu  16658  ushgredgedg  16672  ushgredgedgloop  16674  usgr2v1e2w  16692  egrsubgr  16709  subumgredg2en  16717  iswlk  16769  wlkl1loop  16804  uspgr2wlkeq  16811  istrl  16831  clwwlkccatlem  16846  clwwlkccat  16847  clwwlknccat  16869  clwwlknonex2lem2  16884  clwwlknonex2  16885  iseupth  16893  eupth2lem3lem6fi  16917  konigsbergssiedgwen  16932  bdfind  17177  repiecele0  17281  repiecege0  17282