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  8464  addcan  8469  apcotr  8898  apadd1  8899  mulext1  8903  divdivap1  9014  divdivap2  9015  div2negap  9026  divneg2ap  9027  ltmulgt11  9155  ltdiv2  9178  squeeze0  9195  nndivtr  9296  nn0n0n1ge2  9665  zdivmul  9686  gtndiv  9691  eluzuzle  9880  eluzp1p1  9898  qdivcl  9993  irrmul  9997  rpgecl  10033  xaddass  10221  xltadd1  10228  xlt2add  10232  lbico1  10282  lbicc2  10336  zltaddlt1le  10360  uzsubsubfz  10401  elfz1b  10446  elfz0ubfz0  10481  fz0fzelfz0  10483  difelfzle  10490  difelfznle  10491  2ffzeq  10497  fzo1fzo0n0  10544  ubmelfzo  10567  fzonn0p1p1  10580  elfzom1p1elfzo  10581  elfzonelfzo  10597  subfzo0  10610  ceiqle  10699  ceilqle  10700  modqval  10710  flqpmodeq  10713  modq0  10715  negqmod0  10717  modqge0  10718  modqlt  10719  modqdiffl  10721  modqmulnn  10728  modqvalp1  10729  modqmuladdnn0  10754  qnegmod  10755  addmodid  10758  modfzo0difsn  10781  addmodlteq  10784  qexpclz  10946  expgt1  10963  expp1zap  10974  expm1ap  10975  expubnd  10982  bernneq2  11048  expnlbnd  11051  mulsubdivbinom2ap  11098  omgadd  11191  hashun  11194  fihashssdif  11208  hashdifpr  11210  fimaxq  11219  ccatval2  11311  ccatval3  11312  ccatval1lsw  11317  ccatval21sw  11318  ccatass  11321  ccatw2s1leng  11351  ccats1val2  11353  ccat2s1fvwd  11360  fzowrddc  11364  swrdval  11365  swrdclg  11367  swrdval2  11368  swrdnd  11376  swrdlen2  11379  swrdfv2  11380  ccatswrd  11387  pfxn0  11405  pfxsuff1eqwrdeq  11416  swrdswrdlem  11421  ccats1pfxeq  11431  ccats1pfxeqrex  11432  ccatopth2  11434  wrd2ind  11440  pfxccatin12lem3  11449  pfxccat3  11451  swrdccat  11452  pfxccatpfx2  11454  pfxccat3a  11455  swrdccat3b  11457  pfxccatid  11458  ccats1pfxeqbi  11459  shftuz  11527  mulreap  11574  redivap  11584  imdivap  11591  resqrtcl  11739  xrmaxltsup  11968  xrmaxaddlem  11970  xrmaxadd  11971  xrlemininf  11981  xrminltinf  11982  climuni  12003  addcn2  12020  mulcn2  12022  efsub  12392  sin02gt0  12475  cos12dec  12479  dvdsval2  12501  addmodlteqALT  12570  modremain  12640  fldivndvdslt  12648  mulgcdr  12739  gcddiv  12740  rpmulgcd  12747  rplpwr  12748  rppwr  12749  nnminle  12756  qredeq  12818  divgcdcoprmex  12824  cncongr1  12825  cncongr2  12826  dvdsnprmd  12847  euclemma  12868  prmexpb  12873  qnumdenbi  12914  eulerth  12955  fermltl  12956  prmdiv  12957  hashgcdlem  12960  odzcllem  12965  vfermltl  12974  reumodprminv  12976  modprm0  12977  modprmn0modprm0  12979  coprimeprodsq  12980  pythagtriplem1  12988  pythagtriplem3  12990  pythagtriplem4  12991  pythagtriplem10  12992  pythagtriplem6  12993  pythagtriplem7  12994  pythagtriplem8  12995  pythagtriplem9  12996  pythagtriplem11  12997  pythagtriplem12  12998  pythagtriplem13  12999  pythagtriplem14  13000  pythagtriplem15  13001  pythagtriplem16  13002  pythagtriplem17  13003  pythagtriplem19  13005  pythagtrip  13006  pcpremul  13016  pcdvdsb  13043  dvdsprmpweqnn  13059  dvdsprmpweqle  13060  difsqpwdvds  13061  pcfaclem  13072  pcbc  13074  4sqlem12  13125  ballotfilemsgt1  13198  ballotfilemieq  13204  ballotfilemfrcn0  13217  unennn  13232  nninfdc  13288  setsex  13328  f1ocpbllem  13574  imasaddfnlemg  13578  imasaddvallemg  13579  ercpbl  13595  erlecpbl  13596  qusaddvallemg  13597  fvprif  13607  xpsfrnel2  13610  plusfvalg  13626  imasmnd  13708  insubm  13740  grpidrcan  13820  grpidlcan  13821  grpsubpropd2  13860  imasgrp2  13863  imasgrp  13864  mulgnnsubcl  13887  mulgnn0subcl  13888  mulgsubcl  13889  mulgaddcom  13899  mulginvcom  13900  mulgnnass  13910  mulgassr  13913  mulgpropdg  13917  submmulg  13919  subgcl  13937  subgsubcl  13938  subgsub  13939  subgmulg  13941  nsgconj  13959  ghmsub  14004  ghmrn  14010  ghmeqker  14024  f1ghm0to0  14025  ablinvadd  14063  ablsub4  14066  abladdsub4  14067  subcmnd  14086  imasabl  14089  pwsinvg  14157  rngcl  14183  imasrng  14195  rng1zrlem  14198  rng1zr  14199  rngen1zr0  14201  srgcl  14213  srg1zr  14230  srgen1zr0  14231  ringcl  14256  crngcom  14257  ringidss  14272  mulgass2  14301  imasring  14307  opprmulg  14314  unitmulclb  14359  unitdvcl  14381  rhmmul  14409  rhmdvdsr  14420  subrngmcl  14455  subrgmcl  14479  subrgdv  14484  subrgugrp  14486  domneq0  14519  scafvalg  14581  lmodprop2d  14622  lssclg  14638  lssvnegcl  14650  lssintclm  14658  sralmod  14724  rnglidlmcl  14754  lidlnegcl  14759  rspssp  14768  rnglidlmsgrp  14771  rnglidlrng  14772  2idlcpblrng  14797  qus2idrng  14799  zndvds  14923  znleval2  14928  psrbaglesupp  14948  psrbaglecl  14950  psrbagaddclfi  14951  psrbagcon  14952  basgen  15071  2basgeng  15073  iuncld  15106  neipsm  15145  opnneissb  15146  opnssneib  15147  iscnp3  15194  cnprcl2k  15197  cnpnei  15210  cncnp2m  15222  cnptoprest  15230  sslm  15238  upxp  15263  cnmpt22  15285  distspace  15326  0met  15375  blvalps  15379  blval  15380  ssblps  15416  ssbl  15417  blpnfctr  15430  blopn  15481  blnei  15483  bdxmet  15492  bdbl  15494  metcnp3  15502  tgqioo  15546  ptolemy  15815  sinq12gt0  15821  sincosq1eq  15830  rpcxpadd  15896  cxpmul  15903  rplogbval  15936  logbleb  15952  logbgcd1irr  15958  logbprmirr  15963  pellexlem1  15971  lgsfvalg  16004  lgsneg1  16024  lgssq  16039  lgsdinn0  16047  gausslemma2dlem1a  16057  2lgs  16103  2lgsoddprmlem2  16105  funvtxdm2domval  16150  funiedgdm2domval  16151  iedgedgg  16182  lpvtx  16200  incistruhgr  16211  ausgrumgrien  16291  ausgrusgrien  16292  umgr2edgneu  16333  ushgredgedg  16347  ushgredgedgloop  16349  usgr2v1e2w  16367  egrsubgr  16384  subumgredg2en  16392  iswlk  16444  wlkl1loop  16479  uspgr2wlkeq  16486  istrl  16506  clwwlkccatlem  16521  clwwlkccat  16522  clwwlknccat  16544  clwwlknonex2lem2  16559  clwwlknonex2  16560  iseupth  16568  eupth2lem3lem6fi  16592  konigsbergssiedgwen  16607  bdfind  16842  repiecele0  16936  repiecege0  16937