Theorem 3ad2ant1 1045

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 1043	1 |- ( ( ph /\ ps /\ 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:  simp1l  1048  simp1r  1049  simp11  1054  simp12  1055  simp13  1056  simp1ll  1087  simp1lr  1088  simp1rl  1089  simp1rr  1090  simp1l1  1117  simp1l2  1118  simp1l3  1119  simp1r1  1120  simp1r2  1121  simp1r3  1122  simp11l  1135  simp11r  1136  simp12l  1137  simp12r  1138  simp13l  1139  simp13r  1140  simp111  1153  simp112  1154  simp113  1155  simp121  1156  simp122  1157  simp123  1158  simp131  1159  simp132  1160  simp133  1161  3anim123i  1211  3jaao  1345  ceqsalt  2842  sbciegft  3075  reupick2  3509  ifbothdc  3659  frirrg  4473  breldmg  4964  fntpg  5414  funimaexglem  5441  fex2  5533  fresaunres2disj  5547  fvun1  5745  fprg  5869  fsnunfv  5887  fnfvima  5923  cocan1  5962  cocan2  5963  mpoeq3dv  6121  fovcld  6160  fvmpopr2d  6192  funexw  6307  mpofvex  6403  poxp  6430  suppval1  6441  suppvalfng  6442  suppvalfn  6443  suppimacnvfn  6448  suppsnopdc  6452  smoiso  6535  tfrlem5  6547  tfrlemibxssdm  6560  tfr1onlembfn  6577  tfri1dALT  6584  tfrcllembfn  6590  rdgon  6619  freccllem  6635  nnawordex  6764  1dom1el  7062  mapxpen  7103  fidceq  7126  fidifsnen  7127  dif1en  7138  en2eqpr  7169  unsnfi  7181  unsnfidcex  7182  unsnfidcel  7183  fisseneq  7197  funisfsupp  7246  ordiso2  7328  updjud  7375  mkvprop  7451  endjudisj  7519  xpdjuen  7527  mulcanenq0ec  7762  prltlu  7804  prarloclem3step  7813  prarloclem5  7817  ltasrg  8087  cnegexlem1  8450  addcan  8455  apcotr  8883  apadd1  8884  mulext1  8888  divdivap1  8999  divdivap2  9000  div2negap  9011  divneg2ap  9012  ltmulgt11  9140  ltdiv2  9163  squeeze0  9180  nndivtr  9281  nn0n0n1ge2  9650  zdivmul  9671  gtndiv  9676  eluzuzle  9865  eluzp1p1  9883  qdivcl  9978  irrmul  9982  rpgecl  10018  xaddass  10205  xltadd1  10212  xlt2add  10216  lbico1  10266  lbicc2  10320  zltaddlt1le  10344  uzsubsubfz  10384  elfz1b  10428  elfz0ubfz0  10463  fz0fzelfz0  10465  difelfzle  10472  difelfznle  10473  2ffzeq  10479  fzo1fzo0n0  10526  ubmelfzo  10549  fzonn0p1p1  10562  elfzom1p1elfzo  10563  elfzonelfzo  10579  subfzo0  10592  ceiqle  10679  ceilqle  10680  modqval  10690  flqpmodeq  10693  modq0  10695  negqmod0  10697  modqge0  10698  modqlt  10699  modqdiffl  10701  modqmulnn  10708  modqvalp1  10709  modqmuladdnn0  10734  qnegmod  10735  addmodid  10738  modfzo0difsn  10761  addmodlteq  10764  qexpclz  10926  expgt1  10943  expp1zap  10954  expm1ap  10955  expubnd  10962  bernneq2  11027  expnlbnd  11030  mulsubdivbinom2ap  11077  omgadd  11170  hashun  11173  fihashssdif  11187  hashdifpr  11189  fimaxq  11198  ccatval2  11290  ccatval3  11291  ccatval1lsw  11296  ccatval21sw  11297  ccatass  11300  ccatw2s1leng  11330  ccats1val2  11332  ccat2s1fvwd  11339  fzowrddc  11343  swrdval  11344  swrdclg  11346  swrdval2  11347  swrdnd  11355  swrdlen2  11358  swrdfv2  11359  ccatswrd  11366  pfxn0  11384  pfxsuff1eqwrdeq  11395  swrdswrdlem  11400  ccats1pfxeq  11410  ccats1pfxeqrex  11411  ccatopth2  11413  wrd2ind  11419  pfxccatin12lem3  11428  pfxccat3  11430  swrdccat  11431  pfxccatpfx2  11433  pfxccat3a  11434  swrdccat3b  11436  pfxccatid  11437  ccats1pfxeqbi  11438  shftuz  11506  mulreap  11553  redivap  11563  imdivap  11570  resqrtcl  11718  xrmaxltsup  11947  xrmaxaddlem  11949  xrmaxadd  11950  xrlemininf  11960  xrminltinf  11961  climuni  11982  addcn2  11999  mulcn2  12001  efsub  12371  sin02gt0  12454  cos12dec  12458  dvdsval2  12480  addmodlteqALT  12549  modremain  12619  fldivndvdslt  12627  mulgcdr  12718  gcddiv  12719  rpmulgcd  12726  rplpwr  12727  rppwr  12728  nnminle  12735  qredeq  12797  divgcdcoprmex  12803  cncongr1  12804  cncongr2  12805  dvdsnprmd  12826  euclemma  12847  prmexpb  12852  qnumdenbi  12893  eulerth  12934  fermltl  12935  prmdiv  12936  hashgcdlem  12939  odzcllem  12944  vfermltl  12953  reumodprminv  12955  modprm0  12956  modprmn0modprm0  12958  coprimeprodsq  12959  pythagtriplem1  12967  pythagtriplem3  12969  pythagtriplem4  12970  pythagtriplem10  12971  pythagtriplem6  12972  pythagtriplem7  12973  pythagtriplem8  12974  pythagtriplem9  12975  pythagtriplem11  12976  pythagtriplem12  12977  pythagtriplem13  12978  pythagtriplem14  12979  pythagtriplem15  12980  pythagtriplem16  12981  pythagtriplem17  12982  pythagtriplem19  12984  pythagtrip  12985  pcpremul  12995  pcdvdsb  13022  dvdsprmpweqnn  13038  dvdsprmpweqle  13039  difsqpwdvds  13040  pcfaclem  13051  pcbc  13053  4sqlem12  13104  unennn  13165  nninfdc  13221  setsex  13261  f1ocpbllem  13540  imasaddfnlemg  13544  imasaddvallemg  13545  ercpbl  13561  erlecpbl  13562  qusaddvallemg  13563  fvprif  13573  xpsfrnel2  13576  plusfvalg  13593  imasmnd  13683  insubm  13715  grpidrcan  13795  grpidlcan  13796  grpsubpropd2  13835  pwsinvg  13842  imasgrp2  13844  imasgrp  13845  mulgnnsubcl  13868  mulgnn0subcl  13869  mulgsubcl  13870  mulgaddcom  13880  mulginvcom  13881  mulgnnass  13891  mulgassr  13894  mulgpropdg  13898  submmulg  13900  subgcl  13918  subgsubcl  13919  subgsub  13920  subgmulg  13922  nsgconj  13940  ghmsub  13985  ghmrn  13991  ghmeqker  14005  f1ghm0to0  14006  ablinvadd  14044  ablsub4  14047  abladdsub4  14048  subcmnd  14067  imasabl  14070  rngcl  14105  imasrng  14117  srgcl  14131  srg1zr  14148  srgen1zr  14149  ringcl  14174  crngcom  14175  ringidss  14190  mulgass2  14219  imasring  14225  opprmulg  14232  unitmulclb  14276  unitdvcl  14298  rhmmul  14326  rhmdvdsr  14337  subrngmcl  14371  subrgmcl  14395  subrgdv  14400  subrgugrp  14402  domneq0  14435  scafvalg  14472  lmodprop2d  14513  lssclg  14529  lssvnegcl  14541  lssintclm  14549  sralmod  14615  rnglidlmcl  14645  lidlnegcl  14650  rspssp  14659  rnglidlmsgrp  14662  rnglidlrng  14663  2idlcpblrng  14688  qus2idrng  14690  zndvds  14814  znleval2  14819  psrbaglesupp  14839  psrbaglecl  14841  psrbagaddclfi  14842  psrbagcon  14843  basgen  14962  2basgeng  14964  iuncld  14997  neipsm  15036  opnneissb  15037  opnssneib  15038  iscnp3  15085  cnprcl2k  15088  cnpnei  15101  cncnp2m  15113  cnptoprest  15121  sslm  15129  upxp  15154  cnmpt22  15176  distspace  15217  0met  15266  blvalps  15270  blval  15271  ssblps  15307  ssbl  15308  blpnfctr  15321  blopn  15372  blnei  15374  bdxmet  15383  bdbl  15385  metcnp3  15393  tgqioo  15437  ptolemy  15706  sinq12gt0  15712  sincosq1eq  15721  rpcxpadd  15787  cxpmul  15794  rplogbval  15827  logbleb  15843  logbgcd1irr  15849  logbprmirr  15854  pellexlem1  15862  lgsfvalg  15895  lgsneg1  15915  lgssq  15930  lgsdinn0  15938  gausslemma2dlem1a  15948  2lgs  15994  2lgsoddprmlem2  15996  funvtxdm2domval  16041  funiedgdm2domval  16042  iedgedgg  16073  lpvtx  16091  incistruhgr  16102  ausgrumgrien  16182  ausgrusgrien  16183  umgr2edgneu  16224  ushgredgedg  16238  ushgredgedgloop  16240  usgr2v1e2w  16258  egrsubgr  16275  subumgredg2en  16283  iswlk  16335  wlkl1loop  16370  uspgr2wlkeq  16377  istrl  16397  clwwlkccatlem  16412  clwwlkccat  16413  clwwlknccat  16435  clwwlknonex2lem2  16450  clwwlknonex2  16451  iseupth  16459  eupth2lem3lem6fi  16483  konigsbergssiedgwen  16498  bdfind  16733  repiecele0  16827  repiecege0  16828