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  3017  reupick2  3446  ifbothdc  3591  frirrg  4382  breldmg  4869  fntpg  5311  funimaexglem  5338  fex2  5423  fvun1  5624  fprg  5742  fsnunfv  5760  fnfvima  5794  cocan1  5831  cocan2  5832  mpoeq3dv  5985  fovcld  6024  fvmpopr2d  6056  funexw  6166  mpofvex  6260  poxp  6287  smoiso  6357  tfrlem5  6369  tfrlemibxssdm  6382  tfr1onlembfn  6399  tfri1dALT  6406  tfrcllembfn  6412  rdgon  6441  freccllem  6457  nnawordex  6584  mapxpen  6906  fidceq  6927  fidifsnen  6928  dif1en  6937  en2eqpr  6965  unsnfi  6977  unsnfidcex  6978  unsnfidcel  6979  fisseneq  6990  ordiso2  7096  updjud  7143  mkvprop  7219  endjudisj  7272  xpdjuen  7280  mulcanenq0ec  7507  prltlu  7549  prarloclem3step  7558  prarloclem5  7562  ltasrg  7832  cnegexlem1  8196  addcan  8201  apcotr  8628  apadd1  8629  mulext1  8633  divdivap1  8744  divdivap2  8745  div2negap  8756  divneg2ap  8757  ltmulgt11  8885  ltdiv2  8908  squeeze0  8925  nndivtr  9026  nn0n0n1ge2  9390  zdivmul  9410  gtndiv  9415  eluzuzle  9603  eluzp1p1  9621  qdivcl  9711  irrmul  9715  rpgecl  9751  xaddass  9938  xltadd1  9945  xlt2add  9949  lbico1  9999  lbicc2  10053  zltaddlt1le  10076  uzsubsubfz  10116  elfz1b  10159  elfz0ubfz0  10194  fz0fzelfz0  10196  difelfzle  10203  difelfznle  10204  2ffzeq  10210  fzo1fzo0n0  10253  ubmelfzo  10270  fzonn0p1p1  10283  elfzom1p1elfzo  10284  elfzonelfzo  10300  subfzo0  10312  ceiqle  10387  ceilqle  10388  modqval  10398  flqpmodeq  10401  modq0  10403  negqmod0  10405  modqge0  10406  modqlt  10407  modqdiffl  10409  modqmulnn  10416  modqvalp1  10417  modqmuladdnn0  10442  qnegmod  10443  addmodid  10446  modfzo0difsn  10469  addmodlteq  10472  qexpclz  10634  expgt1  10651  expp1zap  10662  expm1ap  10663  expubnd  10670  bernneq2  10735  expnlbnd  10738  mulsubdivbinom2ap  10785  omgadd  10876  hashun  10879  fihashssdif  10892  hashdifpr  10894  fimaxq  10901  shftuz  10964  mulreap  11011  redivap  11021  imdivap  11028  resqrtcl  11176  xrmaxltsup  11404  xrmaxaddlem  11406  xrmaxadd  11407  xrlemininf  11417  xrminltinf  11418  climuni  11439  addcn2  11456  mulcn2  11458  efsub  11827  sin02gt0  11910  cos12dec  11914  dvdsval2  11936  addmodlteqALT  12004  modremain  12073  fldivndvdslt  12079  mulgcdr  12158  gcddiv  12159  rpmulgcd  12166  rplpwr  12167  rppwr  12168  nnminle  12175  qredeq  12237  divgcdcoprmex  12243  cncongr1  12244  cncongr2  12245  dvdsnprmd  12266  euclemma  12287  prmexpb  12292  qnumdenbi  12333  eulerth  12374  fermltl  12375  prmdiv  12376  hashgcdlem  12379  odzcllem  12383  vfermltl  12392  reumodprminv  12394  modprm0  12395  modprmn0modprm0  12397  coprimeprodsq  12398  pythagtriplem1  12406  pythagtriplem3  12408  pythagtriplem4  12409  pythagtriplem10  12410  pythagtriplem6  12411  pythagtriplem7  12412  pythagtriplem8  12413  pythagtriplem9  12414  pythagtriplem11  12415  pythagtriplem12  12416  pythagtriplem13  12417  pythagtriplem14  12418  pythagtriplem15  12419  pythagtriplem16  12420  pythagtriplem17  12421  pythagtriplem19  12423  pythagtrip  12424  pcpremul  12434  pcdvdsb  12461  dvdsprmpweqnn  12477  dvdsprmpweqle  12478  difsqpwdvds  12479  pcfaclem  12490  pcbc  12492  4sqlem12  12543  unennn  12557  nninfdc  12613  setsex  12653  f1ocpbllem  12896  imasaddfnlemg  12900  imasaddvallemg  12901  ercpbl  12917  erlecpbl  12918  qusaddvallemg  12919  fvprif  12929  xpsfrnel2  12932  plusfvalg  12949  insubm  13060  grpidrcan  13140  grpidlcan  13141  grpsubpropd2  13180  imasgrp2  13183  imasgrp  13184  mulgnnsubcl  13207  mulgnn0subcl  13208  mulgsubcl  13209  mulgaddcom  13219  mulginvcom  13220  mulgnnass  13230  mulgassr  13233  mulgpropdg  13237  submmulg  13239  subgcl  13257  subgsubcl  13258  subgsub  13259  subgmulg  13261  nsgconj  13279  ghmsub  13324  ghmrn  13330  ghmeqker  13344  f1ghm0to0  13345  ablinvadd  13383  ablsub4  13386  abladdsub4  13387  subcmnd  13406  imasabl  13409  rngcl  13443  imasrng  13455  srgcl  13469  srg1zr  13486  srgen1zr  13487  ringcl  13512  crngcom  13513  ringidss  13528  mulgass2  13557  imasring  13563  opprmulg  13570  unitmulclb  13613  unitdvcl  13635  rhmmul  13663  rhmdvdsr  13674  subrngmcl  13708  subrgmcl  13732  subrgdv  13737  subrgugrp  13739  domneq0  13771  scafvalg  13806  lmodprop2d  13847  lssclg  13863  lssvnegcl  13875  lssintclm  13883  sralmod  13949  rnglidlmcl  13979  lidlnegcl  13984  rspssp  13993  rnglidlmsgrp  13996  rnglidlrng  13997  2idlcpblrng  14022  qus2idrng  14024  zndvds  14148  znleval2  14153  basgen  14259  2basgeng  14261  iuncld  14294  neipsm  14333  opnneissb  14334  opnssneib  14335  iscnp3  14382  cnprcl2k  14385  cnpnei  14398  cncnp2m  14410  cnptoprest  14418  sslm  14426  upxp  14451  cnmpt22  14473  distspace  14514  0met  14563  blvalps  14567  blval  14568  ssblps  14604  ssbl  14605  blpnfctr  14618  blopn  14669  blnei  14671  bdxmet  14680  bdbl  14682  metcnp3  14690  tgqioo  14734  ptolemy  15000  sinq12gt0  15006  sincosq1eq  15015  rpcxpadd  15081  cxpmul  15088  rplogbval  15118  logbleb  15134  logbgcd1irr  15140  logbprmirr  15145  lgsfvalg  15162  lgsneg1  15182  lgssq  15197  lgsdinn0  15205  gausslemma2dlem1a  15215  2lgs  15261  2lgsoddprmlem2  15263  bdfind  15508  1dom1el  15553