Theorem 3ad2ant2 960

Description: Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)

Hypothesis

Ref	Expression
3ad2ant.1	|- ( ph -> ch )

Assertion

Ref	Expression
3ad2ant2	|- ( ( ps /\ ph /\ th ) -> ch )

Proof of Theorem 3ad2ant2

Step	Hyp	Ref	Expression
1		3ad2ant.1	. . 3 |- ( ph -> ch )
2	1	adantr 270	. 2 |- ( ( ph /\ th ) -> ch )
3	2	3adant1 956	1 |- ( ( ps /\ ph /\ 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:  simp2l  964  simp2r  965  simp21  971  simp22  972  simp23  973  simp2ll  1005  simp2lr  1006  simp2rl  1007  simp2rr  1008  simp2l1  1037  simp2l2  1038  simp2l3  1039  simp2r1  1040  simp2r2  1041  simp2r3  1042  simp21l  1055  simp21r  1056  simp22l  1057  simp22r  1058  simp23l  1059  simp23r  1060  simp211  1076  simp212  1077  simp213  1078  simp221  1079  simp222  1080  simp223  1081  simp231  1082  simp232  1083  simp233  1084  3anim123i  1123  3jaao  1239  ceqsalt  2625  vtoclgft  2649  vtoclegft  2670  ifbothdc  3380  frirrg  4105  elirr  4284  en2lp  4297  reg3exmidlemwe  4321  sotri3  4743  funtpg  4970  fnprg  4974  fntpg  4975  funimaexglem  5002  fnco  5027  fvun1  5260  oprssov  5662  caovimo  5714  rdgivallem  5991  f1dom2g  6259  ordiso2  6446  distrnqg  6577  distrnq0  6649  prarloclem5  6690  cauappcvgprlemlol  6837  cauappcvgprlemupu  6839  caucvgprlemlol  6860  caucvgprlemupu  6862  caucvgprprlemlol  6888  caucvgprprlemupu  6890  cnegexlem2  7284  apcotr  7707  apadd1  7708  mulext1  7712  div2negap  7823  ltdiv2  7965  nndivtr  8080  zdivmul  8437  gtndiv  8442  fzind  8462  eluzuzle  8627  eluzp1p1  8644  peano2uz  8671  qdivcl  8728  irrmul  8732  ledivge1le  8803  xrre2  8888  ubioc1  8952  ubicc2  9007  zltaddlt1le  9028  uzsubsubfz  9066  elfz1b  9107  fzp1nel  9121  fz0fzdiffz0  9141  difelfzle  9145  elfzo0  9191  elfzonlteqm1  9219  fzonn0p1p1  9222  fzosplitprm1  9243  fzoshftral  9247  subfzo0  9251  ceiqle  9315  modqval  9326  modqvalr  9327  flqpmodeq  9329  modq0  9331  mulqmod0  9332  negqmod0  9333  modqge0  9334  modqlt  9335  modqelico  9336  modqdiffl  9337  modqmulnn  9344  modqvalp1  9345  modqmuladdnn0  9370  qnegmod  9371  addmodid  9374  q2submod  9387  modifeq2int  9388  modfzo0difsn  9397  addmodlteq  9400  expival  9478  redivap  9761  imdivap  9768  climuni  10132  mulcn2  10151  summodnegmod  10226  divalglemex  10322  divalg  10324  modremain  10329  ndvdssub  10330  fldivndvdslt  10335  nndvdslegcd  10357  dfgcd2  10403  mulgcd  10405  mulgcdr  10407  gcddiv  10408  rplpwr  10416  rppwr  10417  qredeq  10478  divgcdcoprmex  10484  cncongr1  10485  cncongr2  10486  pw2dvdslemn  10543