Theorem 3ad2ant2 1043

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

Syntax hints:   -> wi 4   /\ w3a 1002

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 1004

This theorem is referenced by:  simp2l  1047  simp2r  1048  simp21  1054  simp22  1055  simp23  1056  simp2ll  1088  simp2lr  1089  simp2rl  1090  simp2rr  1091  simp2l1  1120  simp2l2  1121  simp2l3  1122  simp2r1  1123  simp2r2  1124  simp2r3  1125  simp21l  1138  simp21r  1139  simp22l  1140  simp22r  1141  simp23l  1142  simp23r  1143  simp211  1159  simp212  1160  simp213  1161  simp221  1162  simp222  1163  simp223  1164  simp231  1165  simp232  1166  simp233  1167  3anim123i  1208  3jaao  1342  ceqsalt  2826  vtoclgft  2851  vtoclegft  2875  ifbothdc  3637  ifnebibdc  3648  frirrg  4441  elirr  4633  en2lp  4646  reg3exmidlemwe  4671  sotri3  5127  funtpg  5372  fnprg  5376  fntpg  5377  funimaexglem  5404  fnco  5431  fvun1  5700  oprssov  6147  caovimo  6199  rdgivallem  6527  fnsnsplitdc  6651  funresdfunsndc  6652  f1dom2g  6907  mapxpen  7009  ssfidc  7099  sbthlemi4  7127  ordiso2  7202  updjud  7249  difinfsn  7267  mkvprop  7325  endjudisj  7392  distrnqg  7574  distrnq0  7646  prarloclem5  7687  cauappcvgprlemlol  7834  cauappcvgprlemupu  7836  caucvgprlemlol  7857  caucvgprlemupu  7859  caucvgprprlemlol  7885  caucvgprprlemupu  7887  cnegexlem2  8322  apcotr  8754  apadd1  8755  mulext1  8759  div2negap  8882  ltdiv2  9034  nndivtr  9152  difgtsumgt  9516  zdivmul  9537  gtndiv  9542  fzind  9562  eluzuzle  9730  eluzp1p1  9748  peano2uz  9778  qdivcl  9838  irrmul  9842  ledivge1le  9922  xrre2  10017  xaddass  10065  xltadd1  10072  xlt2add  10076  ubioc1  10125  ubicc2  10181  zltaddlt1le  10203  uzsubsubfz  10243  elfz1b  10286  fzp1nel  10300  fz0fzdiffz0  10326  difelfzle  10330  elfzo0  10382  elfzonlteqm1  10416  fzonn0p1p1  10419  fzosplitprm1  10440  fzoshftral  10444  subfzo0  10448  ceiqle  10535  modqval  10546  modqvalr  10547  flqpmodeq  10549  modq0  10551  mulqmod0  10552  negqmod0  10553  modqge0  10554  modqlt  10555  modqelico  10556  modqdiffl  10557  modqmulnn  10564  modqvalp1  10565  modqmuladdnn0  10590  qnegmod  10591  addmodid  10594  q2submod  10607  modifeq2int  10608  modfzo0difsn  10617  addmodlteq  10620  mulsubdivbinom2ap  10933  omgadd  11024  hashun  11027  ccatass  11143  lswccatn0lsw  11146  ccats1val2  11171  swrd00g  11181  swrdval2  11183  swrdlen  11184  swrdfv  11185  swrdfv0  11186  swrdnd  11191  swrdlen2  11194  swrdfv2  11195  swrdsbslen  11198  swrdspsleq  11199  ccatswrd  11202  pfxfv  11216  pfxn0  11220  pfxnd  11221  pfxsuff1eqwrdeq  11231  pfxpfx  11240  ccats1pfxeq  11246  ccatopth2  11249  wrd2ind  11255  pfxccatin12lem3  11264  pfxccat3  11266  swrdccat  11267  pfxccat3a  11270  redivap  11385  imdivap  11392  xrmaxltsup  11769  xrmaxadd  11772  xrlemininf  11782  xrminltinf  11783  climuni  11804  mulcn2  11823  fsumsplitsnun  11930  prodfap0  12056  fprodabs  12127  efsub  12192  cos12dec  12279  dvdsmodexp  12306  summodnegmod  12333  divalglemex  12433  divalg  12435  modremain  12440  ndvdssub  12441  fldivndvdslt  12448  bitsfzo  12466  nndvdslegcd  12486  dfgcd2  12535  mulgcd  12537  mulgcdr  12539  gcddiv  12540  rplpwr  12548  rppwr  12549  qredeq  12618  divgcdcoprmex  12624  cncongr1  12625  cncongr2  12626  pw2dvdslemn  12687  hashgcdlem  12760  modprm0  12777  modprmn0modprm0  12779  pythagtriplem1  12788  pythagtriplem3  12790  pythagtriplem10  12792  pythagtriplem6  12793  pythagtriplem7  12794  pythagtriplem11  12797  pythagtriplem12  12798  pythagtriplem13  12799  pythagtriplem14  12800  pythagtriplem19  12805  pythagtrip  12806  dvdsprmpweqnn  12859  difsqpwdvds  12861  pcfaclem  12872  pcbc  12874  unennn  12968  ptex  13297  imasaddvallemg  13348  fvprif  13376  mgmsscl  13394  insubm  13518  mulginvcom  13684  mulgassr  13697  mulgmodid  13698  quselbasg  13767  ghmnsgima  13805  ringrng  13999  rmodislmodlem  14314  rmodislmod  14315  lssincl  14349  sralmod  14414  rnglidlmmgm  14460  rnglidlmsgrp  14461  rnglidlrng  14462  2idlcpblrng  14487  psrbaglesuppg  14636  ntrin  14798  elnei  14826  restco  14848  cnpnei  14893  cncnp2m  14905  sslm  14921  upxp  14946  blres  15108  metcnp3  15185  tgqioo  15229  dvply1  15439  ptolemy  15498  cxpcom  15612  logbgcd1irr  15641  logbprmirr  15646  lgslem1  15679  lgsneg  15703  lgsdilem  15706  lgsdir  15714  lgssq2  15720  lgsdirnn0  15726  gausslemma2dlem1a  15737  2lgslem1a1  15765  incistruhgr  15890  upgrex  15903  uhgr2edg  16004  iedginwlk  16068  uspgr2wlkeq2  16077