Theorem 3ad2ant1 959

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

Syntax hints:   -> wi 4   /\ w3a 919

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

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  simp1l  962  simp1r  963  simp11  968  simp12  969  simp13  970  simp1ll  1001  simp1lr  1002  simp1rl  1003  simp1rr  1004  simp1l1  1031  simp1l2  1032  simp1l3  1033  simp1r1  1034  simp1r2  1035  simp1r3  1036  simp11l  1049  simp11r  1050  simp12l  1051  simp12r  1052  simp13l  1053  simp13r  1054  simp111  1067  simp112  1068  simp113  1069  simp121  1070  simp122  1071  simp123  1072  simp131  1073  simp132  1074  simp133  1075  3anim123i  1123  3jaao  1239  ceqsalt  2625  sbciegft  2844  reupick2  3250  ifbothdc  3380  frirrg  4105  breldmg  4559  fntpg  4975  funimaexglem  5002  fex2  5079  fvun1  5260  fprg  5367  fsnunfv  5384  fnfvima  5414  cocan1  5447  cocan2  5448  mpt2fvex  5849  poxp  5873  smoiso  5940  tfrlem5  5953  tfrlemibxssdm  5964  nnawordex  6124  fidceq  6354  fidifsnen  6355  dif1en  6364  en2eqpr  6380  unsnfi  6384  unsnfidcex  6385  unsnfidcel  6386  ordiso2  6446  mulcanenq0ec  6635  prltlu  6677  prarloclem3step  6686  prarloclem5  6690  ltasrg  6947  cnegexlem1  7283  addcan  7288  apcotr  7707  apadd1  7708  mulext1  7712  divdivap1  7811  divdivap2  7812  div2negap  7823  divneg2ap  7824  ltmulgt11  7942  ltdiv2  7965  squeeze0  7982  nndivtr  8080  nn0n0n1ge2  8418  zdivmul  8437  gtndiv  8442  eluzuzle  8627  eluzp1p1  8644  qdivcl  8728  irrmul  8732  rpgecl  8762  lbico1  8953  lbicc2  9006  zltaddlt1le  9028  uzsubsubfz  9066  elfz1b  9107  elfz0ubfz0  9136  fz0fzelfz0  9138  difelfzle  9145  difelfznle  9146  2ffzeq  9151  fzo1fzo0n0  9192  ubmelfzo  9209  fzonn0p1p1  9222  elfzom1p1elfzo  9223  elfzonelfzo  9239  subfzo0  9251  ceiqle  9315  ceilqle  9316  modqval  9326  flqpmodeq  9329  modq0  9331  negqmod0  9333  modqge0  9334  modqlt  9335  modqdiffl  9337  modqmulnn  9344  modqvalp1  9345  modqmuladdnn0  9370  qnegmod  9371  addmodid  9374  modfzo0difsn  9397  addmodlteq  9400  qexpclz  9497  expgt1  9514  expp1zap  9525  expm1ap  9526  expubnd  9533  bernneq2  9594  expnlbnd  9597  shftuz  9705  mulreap  9751  redivap  9761  imdivap  9768  resqrtcl  9915  climuni  10132  addcn2  10149  mulcn2  10151  dvdsval2  10198  addmodlteqALT  10259  modremain  10329  fldivndvdslt  10335  mulgcdr  10407  gcddiv  10408  rpmulgcd  10415  rplpwr  10416  rppwr  10417  qredeq  10478  divgcdcoprmex  10484  cncongr1  10485  cncongr2  10486  dvdsnprmd  10507  euclemma  10525  prmexpb  10530  bdfind  10741