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  3076  reupick2  3511  ifbothdc  3661  frirrg  4476  breldmg  4967  fntpg  5417  funimaexglem  5444  fex2  5536  fresaunres2disj  5550  fvun1  5748  fprg  5872  fsnunfv  5890  fnfvima  5926  cocan1  5966  cocan2  5967  mpoeq3dv  6127  fovcld  6166  fvmpopr2d  6198  funexw  6314  mpofvex  6414  poxp  6441  suppval1  6452  suppvalfng  6453  suppvalfn  6454  suppimacnvfn  6459  suppsnopdc  6463  smoiso  6546  tfrlem5  6558  tfrlemibxssdm  6571  tfr1onlembfn  6588  tfri1dALT  6595  tfrcllembfn  6601  rdgon  6630  freccllem  6646  nnawordex  6775  1dom1el  7073  mapxpen  7114  fidceq  7137  fidifsnen  7138  dif1en  7149  en2eqpr  7180  unsnfi  7192  unsnfidcex  7193  unsnfidcel  7194  fisseneq  7208  funisfsupp  7257  ordiso2  7339  updjud  7386  mkvprop  7462  endjudisj  7530  xpdjuen  7538  mulcanenq0ec  7776  prltlu  7818  prarloclem3step  7827  prarloclem5  7831  ltasrg  8101  cnegexlem1  8465  addcan  8470  apcotr  8899  apadd1  8900  mulext1  8904  divdivap1  9017  divdivap2  9018  div2negap  9029  divneg2ap  9030  ltmulgt11  9158  ltdiv2  9181  squeeze0  9198  nndivtr  9299  nn0n0n1ge2  9668  zdivmul  9689  gtndiv  9694  eluzuzle  9883  eluzp1p1  9901  qdivcl  9996  irrmul  10000  rpgecl  10036  xaddass  10224  xltadd1  10231  xlt2add  10235  lbico1  10285  lbicc2  10339  zltaddlt1le  10363  uzsubsubfz  10404  elfz1b  10449  elfz0ubfz0  10484  fz0fzelfz0  10486  difelfzle  10493  difelfznle  10494  2ffzeq  10500  fzo1fzo0n0  10547  ubmelfzo  10570  fzonn0p1p1  10583  elfzom1p1elfzo  10584  elfzonelfzo  10600  subfzo0  10613  ceiqle  10702  ceilqle  10703  modqval  10713  flqpmodeq  10716  modq0  10718  negqmod0  10720  modqge0  10721  modqlt  10722  modqdiffl  10724  modqmulnn  10731  modqvalp1  10732  modqmuladdnn0  10757  qnegmod  10758  addmodid  10761  modfzo0difsn  10784  addmodlteq  10787  qexpclz  10949  expgt1  10966  expp1zap  10977  expm1ap  10978  expubnd  10985  bernneq2  11051  expnlbnd  11054  mulsubdivbinom2ap  11101  omgadd  11194  hashun  11197  fihashssdif  11211  hashdifpr  11213  fimaxq  11222  ccatval2  11314  ccatval3  11315  ccatval1lsw  11320  ccatval21sw  11321  ccatass  11324  ccatw2s1leng  11354  ccats1val2  11356  ccat2s1fvwd  11363  fzowrddc  11367  swrdval  11368  swrdclg  11370  swrdval2  11371  swrdnd  11379  swrdlen2  11382  swrdfv2  11383  ccatswrd  11390  pfxn0  11408  pfxsuff1eqwrdeq  11419  swrdswrdlem  11424  ccats1pfxeq  11434  ccats1pfxeqrex  11435  ccatopth2  11437  wrd2ind  11443  pfxccatin12lem3  11452  pfxccat3  11454  swrdccat  11455  pfxccatpfx2  11457  pfxccat3a  11458  swrdccat3b  11460  pfxccatid  11461  ccats1pfxeqbi  11462  shftuz  11530  mulreap  11577  redivap  11587  imdivap  11594  resqrtcl  11742  xrmaxltsup  11971  xrmaxaddlem  11973  xrmaxadd  11974  xrlemininf  11984  xrminltinf  11985  climuni  12006  addcn2  12023  mulcn2  12025  efsub  12395  sin02gt0  12478  cos12dec  12482  dvdsval2  12504  addmodlteqALT  12573  modremain  12643  fldivndvdslt  12651  mulgcdr  12742  gcddiv  12743  rpmulgcd  12750  rplpwr  12751  rppwr  12752  nnminle  12759  qredeq  12821  divgcdcoprmex  12827  cncongr1  12828  cncongr2  12829  dvdsnprmd  12850  euclemma  12871  prmexpb  12876  qnumdenbi  12917  eulerth  12958  fermltl  12959  prmdiv  12960  hashgcdlem  12963  odzcllem  12968  vfermltl  12977  reumodprminv  12979  modprm0  12980  modprmn0modprm0  12982  coprimeprodsq  12983  pythagtriplem1  12991  pythagtriplem3  12993  pythagtriplem4  12994  pythagtriplem10  12995  pythagtriplem6  12996  pythagtriplem7  12997  pythagtriplem8  12998  pythagtriplem9  12999  pythagtriplem11  13000  pythagtriplem12  13001  pythagtriplem13  13002  pythagtriplem14  13003  pythagtriplem15  13004  pythagtriplem16  13005  pythagtriplem17  13006  pythagtriplem19  13008  pythagtrip  13009  pcpremul  13019  pcdvdsb  13046  dvdsprmpweqnn  13062  dvdsprmpweqle  13063  difsqpwdvds  13064  pcfaclem  13075  pcbc  13077  4sqlem12  13128  ballotfilemsgt1  13201  ballotfilemieq  13207  ballotfilemfrcn0  13220  unennn  13235  nninfdc  13291  setsex  13331  f1ocpbllem  13577  imasaddfnlemg  13581  imasaddvallemg  13582  ercpbl  13598  erlecpbl  13599  qusaddvallemg  13600  fvprif  13610  xpsfrnel2  13613  plusfvalg  13629  imasmnd  13711  insubm  13743  grpidrcan  13823  grpidlcan  13824  grpsubpropd2  13863  imasgrp2  13866  imasgrp  13867  mulgnnsubcl  13890  mulgnn0subcl  13891  mulgsubcl  13892  mulgaddcom  13902  mulginvcom  13903  mulgnnass  13913  mulgassr  13916  mulgpropdg  13920  submmulg  13922  subgcl  13940  subgsubcl  13941  subgsub  13942  subgmulg  13944  nsgconj  13962  ghmsub  14007  ghmrn  14013  ghmeqker  14027  f1ghm0to0  14028  ablinvadd  14066  ablsub4  14069  abladdsub4  14070  subcmnd  14089  imasabl  14092  pwsinvg  14160  rngcl  14186  imasrng  14198  rng1zrlem  14201  rng1zr  14202  rngen1zr0  14204  srgcl  14216  srg1zr  14233  srgen1zr0  14234  ringcl  14259  crngcom  14260  ringidss  14275  mulgass2  14304  imasring  14310  opprmulg  14317  unitmulclb  14362  unitdvcl  14384  rhmmul  14412  rhmdvdsr  14423  subrngmcl  14458  subrgmcl  14482  subrgdv  14487  subrgugrp  14489  domneq0  14522  scafvalg  14584  lmodprop2d  14625  lssclg  14641  lssvnegcl  14653  lssintclm  14661  sralmod  14727  rnglidlmcl  14757  lidlnegcl  14762  rspssp  14771  rnglidlmsgrp  14774  rnglidlrng  14775  2idlcpblrng  14800  qus2idrng  14802  zndvds  14926  znleval2  14931  psrbaglesupp  14951  psrbaglecl  14953  psrbagaddclfi  14954  psrbagcon  14955  basgen  15074  2basgeng  15076  iuncld  15109  neipsm  15148  opnneissb  15149  opnssneib  15150  iscnp3  15197  cnprcl2k  15200  cnpnei  15213  cncnp2m  15225  cnptoprest  15233  sslm  15241  upxp  15266  cnmpt22  15288  distspace  15329  0met  15378  blvalps  15382  blval  15383  ssblps  15419  ssbl  15420  blpnfctr  15433  blopn  15484  blnei  15486  bdxmet  15495  bdbl  15497  metcnp3  15505  tgqioo  15549  ptolemy  15818  sinq12gt0  15824  sincosq1eq  15833  rpcxpadd  15899  cxpmul  15906  rplogbval  15939  logbleb  15955  logbgcd1irr  15961  logbprmirr  15966  pellexlem1  15974  lgsfvalg  16007  lgsneg1  16027  lgssq  16042  lgsdinn0  16050  gausslemma2dlem1a  16060  2lgs  16106  2lgsoddprmlem2  16108  funvtxdm2domval  16153  funiedgdm2domval  16154  iedgedgg  16185  lpvtx  16203  incistruhgr  16214  ausgrumgrien  16294  ausgrusgrien  16295  umgr2edgneu  16336  ushgredgedg  16350  ushgredgedgloop  16352  usgr2v1e2w  16370  egrsubgr  16387  subumgredg2en  16395  iswlk  16447  wlkl1loop  16482  uspgr2wlkeq  16489  istrl  16509  clwwlkccatlem  16524  clwwlkccat  16525  clwwlknccat  16547  clwwlknonex2lem2  16562  clwwlknonex2  16563  iseupth  16571  eupth2lem3lem6fi  16595  konigsbergssiedgwen  16610  bdfind  16855  repiecele0  16949  repiecege0  16950