Theorem 3ad2ant2 1014

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 1010	1 |- ( ( ps /\ ph /\ th ) -> ch )

Syntax hints:   -> wi 4   /\ w3a 973

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 975

This theorem is referenced by:  simp2l  1018  simp2r  1019  simp21  1025  simp22  1026  simp23  1027  simp2ll  1059  simp2lr  1060  simp2rl  1061  simp2rr  1062  simp2l1  1091  simp2l2  1092  simp2l3  1093  simp2r1  1094  simp2r2  1095  simp2r3  1096  simp21l  1109  simp21r  1110  simp22l  1111  simp22r  1112  simp23l  1113  simp23r  1114  simp211  1130  simp212  1131  simp213  1132  simp221  1133  simp222  1134  simp223  1135  simp231  1136  simp232  1137  simp233  1138  3anim123i  1179  3jaao  1303  ceqsalt  2756  vtoclgft  2780  vtoclegft  2802  ifbothdc  3558  frirrg  4335  elirr  4525  en2lp  4538  reg3exmidlemwe  4563  sotri3  5009  funtpg  5249  fnprg  5253  fntpg  5254  funimaexglem  5281  fnco  5306  fvun1  5562  oprssov  5994  caovimo  6046  rdgivallem  6360  fnsnsplitdc  6484  funresdfunsndc  6485  f1dom2g  6734  mapxpen  6826  ssfidc  6912  sbthlemi4  6937  ordiso2  7012  updjud  7059  difinfsn  7077  mkvprop  7134  endjudisj  7187  distrnqg  7349  distrnq0  7421  prarloclem5  7462  cauappcvgprlemlol  7609  cauappcvgprlemupu  7611  caucvgprlemlol  7632  caucvgprlemupu  7634  caucvgprprlemlol  7660  caucvgprprlemupu  7662  cnegexlem2  8095  apcotr  8526  apadd1  8527  mulext1  8531  div2negap  8652  ltdiv2  8803  nndivtr  8920  difgtsumgt  9281  zdivmul  9302  gtndiv  9307  fzind  9327  eluzuzle  9495  eluzp1p1  9512  peano2uz  9542  qdivcl  9602  irrmul  9606  ledivge1le  9683  xrre2  9778  xaddass  9826  xltadd1  9833  xlt2add  9837  ubioc1  9886  ubicc2  9942  zltaddlt1le  9964  uzsubsubfz  10003  elfz1b  10046  fzp1nel  10060  fz0fzdiffz0  10086  difelfzle  10090  elfzo0  10138  elfzonlteqm1  10166  fzonn0p1p1  10169  fzosplitprm1  10190  fzoshftral  10194  subfzo0  10198  ceiqle  10269  modqval  10280  modqvalr  10281  flqpmodeq  10283  modq0  10285  mulqmod0  10286  negqmod0  10287  modqge0  10288  modqlt  10289  modqelico  10290  modqdiffl  10291  modqmulnn  10298  modqvalp1  10299  modqmuladdnn0  10324  qnegmod  10325  addmodid  10328  q2submod  10341  modifeq2int  10342  modfzo0difsn  10351  addmodlteq  10354  omgadd  10737  hashun  10740  redivap  10838  imdivap  10845  xrmaxltsup  11221  xrmaxadd  11224  xrlemininf  11234  xrminltinf  11235  climuni  11256  mulcn2  11275  fsumsplitsnun  11382  prodfap0  11508  fprodabs  11579  efsub  11644  cos12dec  11730  dvdsmodexp  11757  summodnegmod  11784  divalglemex  11881  divalg  11883  modremain  11888  ndvdssub  11889  fldivndvdslt  11894  nndvdslegcd  11920  dfgcd2  11969  mulgcd  11971  mulgcdr  11973  gcddiv  11974  rplpwr  11982  rppwr  11983  qredeq  12050  divgcdcoprmex  12056  cncongr1  12057  cncongr2  12058  pw2dvdslemn  12119  hashgcdlem  12192  modprm0  12208  modprmn0modprm0  12210  pythagtriplem1  12219  pythagtriplem3  12221  pythagtriplem10  12223  pythagtriplem6  12224  pythagtriplem7  12225  pythagtriplem11  12228  pythagtriplem12  12229  pythagtriplem13  12230  pythagtriplem14  12231  pythagtriplem19  12236  pythagtrip  12237  dvdsprmpweqnn  12289  difsqpwdvds  12291  pcfaclem  12301  pcbc  12303  unennn  12352  mgmsscl  12615  insubm  12703  ntrin  12918  elnei  12946  restco  12968  cnpnei  13013  cncnp2m  13025  sslm  13041  upxp  13066  blres  13228  metcnp3  13305  tgqioo  13341  ptolemy  13539  cxpcom  13651  logbgcd1irr  13679  logbprmirr  13684  lgslem1  13695  lgsneg  13719  lgsdilem  13722  lgsdir  13730  lgssq2  13736  lgsdirnn0  13742