Theorem 3ad2ant2 1022

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

Syntax hints:   -> wi 4   /\ w3a 981

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

This theorem depends on definitions:  df-bi 117  df-3an 983

This theorem is referenced by:  simp2l  1026  simp2r  1027  simp21  1033  simp22  1034  simp23  1035  simp2ll  1067  simp2lr  1068  simp2rl  1069  simp2rr  1070  simp2l1  1099  simp2l2  1100  simp2l3  1101  simp2r1  1102  simp2r2  1103  simp2r3  1104  simp21l  1117  simp21r  1118  simp22l  1119  simp22r  1120  simp23l  1121  simp23r  1122  simp211  1138  simp212  1139  simp213  1140  simp221  1141  simp222  1142  simp223  1143  simp231  1144  simp232  1145  simp233  1146  3anim123i  1187  3jaao  1321  ceqsalt  2798  vtoclgft  2823  vtoclegft  2845  ifbothdc  3605  ifnebibdc  3615  frirrg  4397  elirr  4589  en2lp  4602  reg3exmidlemwe  4627  sotri3  5081  funtpg  5325  fnprg  5329  fntpg  5330  funimaexglem  5357  fnco  5384  fvun1  5645  oprssov  6088  caovimo  6140  rdgivallem  6467  fnsnsplitdc  6591  funresdfunsndc  6592  f1dom2g  6847  mapxpen  6945  ssfidc  7034  sbthlemi4  7062  ordiso2  7137  updjud  7184  difinfsn  7202  mkvprop  7260  endjudisj  7322  distrnqg  7500  distrnq0  7572  prarloclem5  7613  cauappcvgprlemlol  7760  cauappcvgprlemupu  7762  caucvgprlemlol  7783  caucvgprlemupu  7785  caucvgprprlemlol  7811  caucvgprprlemupu  7813  cnegexlem2  8248  apcotr  8680  apadd1  8681  mulext1  8685  div2negap  8808  ltdiv2  8960  nndivtr  9078  difgtsumgt  9442  zdivmul  9463  gtndiv  9468  fzind  9488  eluzuzle  9656  eluzp1p1  9674  peano2uz  9704  qdivcl  9764  irrmul  9768  ledivge1le  9848  xrre2  9943  xaddass  9991  xltadd1  9998  xlt2add  10002  ubioc1  10051  ubicc2  10107  zltaddlt1le  10129  uzsubsubfz  10169  elfz1b  10212  fzp1nel  10226  fz0fzdiffz0  10252  difelfzle  10256  elfzo0  10306  elfzonlteqm1  10339  fzonn0p1p1  10342  fzosplitprm1  10363  fzoshftral  10367  subfzo0  10371  ceiqle  10458  modqval  10469  modqvalr  10470  flqpmodeq  10472  modq0  10474  mulqmod0  10475  negqmod0  10476  modqge0  10477  modqlt  10478  modqelico  10479  modqdiffl  10480  modqmulnn  10487  modqvalp1  10488  modqmuladdnn0  10513  qnegmod  10514  addmodid  10517  q2submod  10530  modifeq2int  10531  modfzo0difsn  10540  addmodlteq  10543  mulsubdivbinom2ap  10856  omgadd  10947  hashun  10950  ccatass  11064  lswccatn0lsw  11067  ccats1val2  11092  swrd00g  11102  swrdval2  11104  swrdlen  11105  swrdfv  11106  swrdfv0  11107  swrdnd  11112  swrdlen2  11115  swrdfv2  11116  swrdsbslen  11119  swrdspsleq  11120  ccatswrd  11123  redivap  11185  imdivap  11192  xrmaxltsup  11569  xrmaxadd  11572  xrlemininf  11582  xrminltinf  11583  climuni  11604  mulcn2  11623  fsumsplitsnun  11730  prodfap0  11856  fprodabs  11927  efsub  11992  cos12dec  12079  dvdsmodexp  12106  summodnegmod  12133  divalglemex  12233  divalg  12235  modremain  12240  ndvdssub  12241  fldivndvdslt  12248  bitsfzo  12266  nndvdslegcd  12286  dfgcd2  12335  mulgcd  12337  mulgcdr  12339  gcddiv  12340  rplpwr  12348  rppwr  12349  qredeq  12418  divgcdcoprmex  12424  cncongr1  12425  cncongr2  12426  pw2dvdslemn  12487  hashgcdlem  12560  modprm0  12577  modprmn0modprm0  12579  pythagtriplem1  12588  pythagtriplem3  12590  pythagtriplem10  12592  pythagtriplem6  12593  pythagtriplem7  12594  pythagtriplem11  12597  pythagtriplem12  12598  pythagtriplem13  12599  pythagtriplem14  12600  pythagtriplem19  12605  pythagtrip  12606  dvdsprmpweqnn  12659  difsqpwdvds  12661  pcfaclem  12672  pcbc  12674  unennn  12768  ptex  13096  imasaddvallemg  13147  fvprif  13175  mgmsscl  13193  insubm  13317  mulginvcom  13483  mulgassr  13496  mulgmodid  13497  quselbasg  13566  ghmnsgima  13604  ringrng  13798  rmodislmodlem  14112  rmodislmod  14113  lssincl  14147  sralmod  14212  rnglidlmmgm  14258  rnglidlmsgrp  14259  rnglidlrng  14260  2idlcpblrng  14285  psrbaglesuppg  14434  ntrin  14596  elnei  14624  restco  14646  cnpnei  14691  cncnp2m  14703  sslm  14719  upxp  14744  blres  14906  metcnp3  14983  tgqioo  15027  dvply1  15237  ptolemy  15296  cxpcom  15410  logbgcd1irr  15439  logbprmirr  15444  lgslem1  15477  lgsneg  15501  lgsdilem  15504  lgsdir  15512  lgssq2  15518  lgsdirnn0  15524  gausslemma2dlem1a  15535  2lgslem1a1  15563