Theorem 3ad2ant2 1004

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

Syntax hints:   -> wi 4   /\ w3a 963

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 965

This theorem is referenced by:  simp2l  1008  simp2r  1009  simp21  1015  simp22  1016  simp23  1017  simp2ll  1049  simp2lr  1050  simp2rl  1051  simp2rr  1052  simp2l1  1081  simp2l2  1082  simp2l3  1083  simp2r1  1084  simp2r2  1085  simp2r3  1086  simp21l  1099  simp21r  1100  simp22l  1101  simp22r  1102  simp23l  1103  simp23r  1104  simp211  1120  simp212  1121  simp213  1122  simp221  1123  simp222  1124  simp223  1125  simp231  1126  simp232  1127  simp233  1128  3anim123i  1167  3jaao  1287  ceqsalt  2715  vtoclgft  2739  vtoclegft  2761  ifbothdc  3509  frirrg  4280  elirr  4464  en2lp  4477  reg3exmidlemwe  4501  sotri3  4945  funtpg  5182  fnprg  5186  fntpg  5187  funimaexglem  5214  fnco  5239  fvun1  5495  oprssov  5920  caovimo  5972  rdgivallem  6286  fnsnsplitdc  6409  funresdfunsndc  6410  f1dom2g  6658  mapxpen  6750  ssfidc  6831  sbthlemi4  6856  ordiso2  6928  updjud  6975  difinfsn  6993  mkvprop  7040  endjudisj  7083  distrnqg  7219  distrnq0  7291  prarloclem5  7332  cauappcvgprlemlol  7479  cauappcvgprlemupu  7481  caucvgprlemlol  7502  caucvgprlemupu  7504  caucvgprprlemlol  7530  caucvgprprlemupu  7532  cnegexlem2  7962  apcotr  8393  apadd1  8394  mulext1  8398  div2negap  8519  ltdiv2  8669  nndivtr  8786  zdivmul  9165  gtndiv  9170  fzind  9190  eluzuzle  9358  eluzp1p1  9375  peano2uz  9405  qdivcl  9462  irrmul  9466  ledivge1le  9543  xrre2  9634  xaddass  9682  xltadd1  9689  xlt2add  9693  ubioc1  9742  ubicc2  9798  zltaddlt1le  9820  uzsubsubfz  9858  elfz1b  9901  fzp1nel  9915  fz0fzdiffz0  9938  difelfzle  9942  elfzo0  9990  elfzonlteqm1  10018  fzonn0p1p1  10021  fzosplitprm1  10042  fzoshftral  10046  subfzo0  10050  ceiqle  10117  modqval  10128  modqvalr  10129  flqpmodeq  10131  modq0  10133  mulqmod0  10134  negqmod0  10135  modqge0  10136  modqlt  10137  modqelico  10138  modqdiffl  10139  modqmulnn  10146  modqvalp1  10147  modqmuladdnn0  10172  qnegmod  10173  addmodid  10176  q2submod  10189  modifeq2int  10190  modfzo0difsn  10199  addmodlteq  10202  omgadd  10580  hashun  10583  redivap  10678  imdivap  10685  xrmaxltsup  11059  xrmaxadd  11062  xrlemininf  11072  xrminltinf  11073  climuni  11094  mulcn2  11113  fsumsplitsnun  11220  prodfap0  11346  efsub  11424  cos12dec  11510  summodnegmod  11560  divalglemex  11655  divalg  11657  modremain  11662  ndvdssub  11663  fldivndvdslt  11668  nndvdslegcd  11690  dfgcd2  11738  mulgcd  11740  mulgcdr  11742  gcddiv  11743  rplpwr  11751  rppwr  11752  qredeq  11813  divgcdcoprmex  11819  cncongr1  11820  cncongr2  11821  pw2dvdslemn  11879  hashgcdlem  11939  unennn  11946  ntrin  12332  elnei  12360  restco  12382  cnpnei  12427  cncnp2m  12439  sslm  12455  upxp  12480  blres  12642  metcnp3  12719  tgqioo  12755  ptolemy  12953  cxpcom  13065  logbgcd1irr  13092  logbprmirr  13097