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  2648  vtoclgft  2672  vtoclegft  2694  ifbothdc  3429  frirrg  4188  elirr  4372  en2lp  4385  reg3exmidlemwe  4409  sotri3  4845  funtpg  5080  fnprg  5084  fntpg  5085  funimaexglem  5112  fnco  5137  fvun1  5385  oprssov  5802  caovimo  5854  rdgivallem  6162  fnsnsplitdc  6280  funresdfunsndc  6281  f1dom2g  6529  mapxpen  6620  ssfidc  6700  sbthlemi4  6725  ordiso2  6784  updjud  6829  distrnqg  7009  distrnq0  7081  prarloclem5  7122  cauappcvgprlemlol  7269  cauappcvgprlemupu  7271  caucvgprlemlol  7292  caucvgprlemupu  7294  caucvgprprlemlol  7320  caucvgprprlemupu  7322  cnegexlem2  7721  apcotr  8147  apadd1  8148  mulext1  8152  div2negap  8265  ltdiv2  8411  nndivtr  8527  zdivmul  8899  gtndiv  8904  fzind  8924  eluzuzle  9090  eluzp1p1  9107  peano2uz  9134  qdivcl  9191  irrmul  9195  ledivge1le  9266  xrre2  9346  ubioc1  9410  ubicc2  9465  zltaddlt1le  9486  uzsubsubfz  9524  elfz1b  9567  fzp1nel  9581  fz0fzdiffz0  9604  difelfzle  9608  elfzo0  9656  elfzonlteqm1  9684  fzonn0p1p1  9687  fzosplitprm1  9708  fzoshftral  9712  subfzo0  9716  ceiqle  9783  modqval  9794  modqvalr  9795  flqpmodeq  9797  modq0  9799  mulqmod0  9800  negqmod0  9801  modqge0  9802  modqlt  9803  modqelico  9804  modqdiffl  9805  modqmulnn  9812  modqvalp1  9813  modqmuladdnn0  9838  qnegmod  9839  addmodid  9842  q2submod  9855  modifeq2int  9856  modfzo0difsn  9865  addmodlteq  9868  omgadd  10273  hashun  10276  redivap  10371  imdivap  10378  climuni  10744  mulcn2  10764  fsumsplitsnun  10876  efsub  11034  summodnegmod  11168  divalglemex  11263  divalg  11265  modremain  11270  ndvdssub  11271  fldivndvdslt  11276  nndvdslegcd  11298  dfgcd2  11344  mulgcd  11346  mulgcdr  11348  gcddiv  11349  rplpwr  11357  rppwr  11358  qredeq  11419  divgcdcoprmex  11425  cncongr1  11426  cncongr2  11427  pw2dvdslemn  11484  hashgcdlem  11544  unennn  11551  ntrin  11887  elnei  11915