Theorem 3ad2ant1 1008

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 274	. 2 |- ( ( ph /\ th ) -> ch )
3	2	3adant2 1006	1 |- ( ( ph /\ ps /\ th ) -> ch )

Syntax hints:   -> wi 4   /\ w3a 968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  simp1l  1011  simp1r  1012  simp11  1017  simp12  1018  simp13  1019  simp1ll  1050  simp1lr  1051  simp1rl  1052  simp1rr  1053  simp1l1  1080  simp1l2  1081  simp1l3  1082  simp1r1  1083  simp1r2  1084  simp1r3  1085  simp11l  1098  simp11r  1099  simp12l  1100  simp12r  1101  simp13l  1102  simp13r  1103  simp111  1116  simp112  1117  simp113  1118  simp121  1119  simp122  1120  simp123  1121  simp131  1122  simp132  1123  simp133  1124  3anim123i  1174  3jaao  1298  ceqsalt  2751  sbciegft  2980  reupick2  3407  ifbothdc  3551  frirrg  4327  breldmg  4809  fntpg  5243  funimaexglem  5270  fex2  5355  fvun1  5551  fprg  5667  fsnunfv  5685  fnfvima  5718  cocan1  5754  cocan2  5755  mpoeq3dv  5904  mpofvex  6168  poxp  6196  smoiso  6266  tfrlem5  6278  tfrlemibxssdm  6291  tfr1onlembfn  6308  tfri1dALT  6315  tfrcllembfn  6321  rdgon  6350  freccllem  6366  nnawordex  6492  mapxpen  6810  fidceq  6831  fidifsnen  6832  dif1en  6841  en2eqpr  6869  unsnfi  6880  unsnfidcex  6881  unsnfidcel  6882  fisseneq  6893  ordiso2  6996  updjud  7043  mkvprop  7118  endjudisj  7162  xpdjuen  7170  mulcanenq0ec  7382  prltlu  7424  prarloclem3step  7433  prarloclem5  7437  ltasrg  7707  cnegexlem1  8069  addcan  8074  apcotr  8501  apadd1  8502  mulext1  8506  divdivap1  8615  divdivap2  8616  div2negap  8627  divneg2ap  8628  ltmulgt11  8755  ltdiv2  8778  squeeze0  8795  nndivtr  8895  nn0n0n1ge2  9257  zdivmul  9277  gtndiv  9282  eluzuzle  9470  eluzp1p1  9487  qdivcl  9577  irrmul  9581  rpgecl  9614  xaddass  9801  xltadd1  9808  xlt2add  9812  lbico1  9862  lbicc2  9916  zltaddlt1le  9939  uzsubsubfz  9978  elfz1b  10021  elfz0ubfz0  10056  fz0fzelfz0  10058  difelfzle  10065  difelfznle  10066  2ffzeq  10072  fzo1fzo0n0  10114  ubmelfzo  10131  fzonn0p1p1  10144  elfzom1p1elfzo  10145  elfzonelfzo  10161  subfzo0  10173  ceiqle  10244  ceilqle  10245  modqval  10255  flqpmodeq  10258  modq0  10260  negqmod0  10262  modqge0  10263  modqlt  10264  modqdiffl  10266  modqmulnn  10273  modqvalp1  10274  modqmuladdnn0  10299  qnegmod  10300  addmodid  10303  modfzo0difsn  10326  addmodlteq  10329  qexpclz  10472  expgt1  10489  expp1zap  10500  expm1ap  10501  expubnd  10508  bernneq2  10572  expnlbnd  10575  omgadd  10711  hashun  10714  fihashssdif  10727  hashdifpr  10729  fimaxq  10736  shftuz  10755  mulreap  10802  redivap  10812  imdivap  10819  resqrtcl  10967  xrmaxltsup  11195  xrmaxaddlem  11197  xrmaxadd  11198  xrlemininf  11208  xrminltinf  11209  climuni  11230  addcn2  11247  mulcn2  11249  efsub  11618  sin02gt0  11700  cos12dec  11704  dvdsval2  11726  addmodlteqALT  11793  modremain  11862  fldivndvdslt  11868  mulgcdr  11947  gcddiv  11948  rpmulgcd  11955  rplpwr  11956  rppwr  11957  nnminle  11964  qredeq  12024  divgcdcoprmex  12030  cncongr1  12031  cncongr2  12032  dvdsnprmd  12053  euclemma  12074  prmexpb  12079  qnumdenbi  12120  eulerth  12161  fermltl  12162  prmdiv  12163  hashgcdlem  12166  odzcllem  12170  vfermltl  12179  reumodprminv  12181  modprm0  12182  modprmn0modprm0  12184  coprimeprodsq  12185  pythagtriplem1  12193  pythagtriplem3  12195  pythagtriplem4  12196  pythagtriplem10  12197  pythagtriplem6  12198  pythagtriplem7  12199  pythagtriplem8  12200  pythagtriplem9  12201  pythagtriplem11  12202  pythagtriplem12  12203  pythagtriplem13  12204  pythagtriplem14  12205  pythagtriplem15  12206  pythagtriplem16  12207  pythagtriplem17  12208  pythagtriplem19  12210  pythagtrip  12211  pcpremul  12221  pcdvdsb  12247  dvdsprmpweqnn  12263  dvdsprmpweqle  12264  difsqpwdvds  12265  pcfaclem  12275  pcbc  12277  unennn  12326  nninfdc  12382  setsex  12422  basgen  12680  2basgeng  12682  iuncld  12715  neipsm  12754  opnneissb  12755  opnssneib  12756  iscnp3  12803  cnprcl2k  12806  cnpnei  12819  cncnp2m  12831  cnptoprest  12839  sslm  12847  upxp  12872  cnmpt22  12894  distspace  12935  0met  12984  blvalps  12988  blval  12989  ssblps  13025  ssbl  13026  blpnfctr  13039  blopn  13090  blnei  13092  bdxmet  13101  bdbl  13103  metcnp3  13111  tgqioo  13147  ptolemy  13345  sinq12gt0  13351  sincosq1eq  13360  rpcxpadd  13426  cxpmul  13433  rplogbval  13463  logbleb  13479  logbgcd1irr  13485  logbprmirr  13490  lgsfvalg  13506  lgsneg1  13526  lgssq  13541  lgsdinn0  13549  bdfind  13788