Theorem 3ad2ant2 966

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 271	. 2 |- ( ( ph /\ th ) -> ch )
3	2	3adant1 962	1 |- ( ( ps /\ ph /\ th ) -> ch )

Syntax hints:   -> wi 4   /\ w3a 925

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

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

This theorem is referenced by:  simp2l  970  simp2r  971  simp21  977  simp22  978  simp23  979  simp2ll  1011  simp2lr  1012  simp2rl  1013  simp2rr  1014  simp2l1  1043  simp2l2  1044  simp2l3  1045  simp2r1  1046  simp2r2  1047  simp2r3  1048  simp21l  1061  simp21r  1062  simp22l  1063  simp22r  1064  simp23l  1065  simp23r  1066  simp211  1082  simp212  1083  simp213  1084  simp221  1085  simp222  1086  simp223  1087  simp231  1088  simp232  1089  simp233  1090  3anim123i  1129  3jaao  1245  ceqsalt  2646  vtoclgft  2670  vtoclegft  2692  ifbothdc  3427  frirrg  4186  elirr  4370  en2lp  4383  reg3exmidlemwe  4407  sotri3  4843  funtpg  5078  fnprg  5082  fntpg  5083  funimaexglem  5110  fnco  5135  fvun1  5383  oprssov  5800  caovimo  5852  rdgivallem  6160  fnsnsplitdc  6278  funresdfunsndc  6279  f1dom2g  6527  mapxpen  6618  ssfidc  6698  sbthlemi4  6723  ordiso2  6782  updjud  6827  distrnqg  7000  distrnq0  7072  prarloclem5  7113  cauappcvgprlemlol  7260  cauappcvgprlemupu  7262  caucvgprlemlol  7283  caucvgprlemupu  7285  caucvgprprlemlol  7311  caucvgprprlemupu  7313  cnegexlem2  7712  apcotr  8138  apadd1  8139  mulext1  8143  div2negap  8256  ltdiv2  8402  nndivtr  8518  zdivmul  8890  gtndiv  8895  fzind  8915  eluzuzle  9081  eluzp1p1  9098  peano2uz  9125  qdivcl  9182  irrmul  9186  ledivge1le  9257  xrre2  9337  ubioc1  9401  ubicc2  9456  zltaddlt1le  9477  uzsubsubfz  9515  elfz1b  9558  fzp1nel  9572  fz0fzdiffz0  9595  difelfzle  9599  elfzo0  9647  elfzonlteqm1  9675  fzonn0p1p1  9678  fzosplitprm1  9699  fzoshftral  9703  subfzo0  9707  ceiqle  9774  modqval  9785  modqvalr  9786  flqpmodeq  9788  modq0  9790  mulqmod0  9791  negqmod0  9792  modqge0  9793  modqlt  9794  modqelico  9795  modqdiffl  9796  modqmulnn  9803  modqvalp1  9804  modqmuladdnn0  9829  qnegmod  9830  addmodid  9833  q2submod  9846  modifeq2int  9847  modfzo0difsn  9856  addmodlteq  9859  omgadd  10264  hashun  10267  redivap  10362  imdivap  10369  climuni  10735  mulcn2  10755  fsumsplitsnun  10867  efsub  11025  summodnegmod  11159  divalglemex  11254  divalg  11256  modremain  11261  ndvdssub  11262  fldivndvdslt  11267  nndvdslegcd  11289  dfgcd2  11335  mulgcd  11337  mulgcdr  11339  gcddiv  11340  rplpwr  11348  rppwr  11349  qredeq  11410  divgcdcoprmex  11416  cncongr1  11417  cncongr2  11418  pw2dvdslemn  11475  hashgcdlem  11535  unennn  11542  ntrin  11878