Theorem ad2ant2l 747

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)

Hypothesis

Ref	Expression
ad2ant2.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
ad2ant2l	⊢ (((𝜃 ∧ 𝜑) ∧ (𝜏 ∧ 𝜓)) → 𝜒)

Proof of Theorem ad2ant2l

Step	Hyp	Ref	Expression
1		ad2ant2.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantrl 717	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒)
3	2	adantll 715	1 ⊢ (((𝜃 ∧ 𝜑) ∧ (𝜏 ∧ 𝜓)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  funcnvqp  6562  mpteqb  6967  soxp  8079  oaass  8496  nadd42  8635  naddel12  8636  undifixp  8882  xpdom2  9010  tcrank  9808  inawinalem  10612  addcanpr  10969  ltsosr  11017  1re  11144  add42  11368  muladd  11582  mulsub  11593  divmuleq  11860  ltmul12a  12011  lemul12b  12012  lemul12a  12013  mulge0b  12026  qaddcl  12915  qmulcl  12917  iooshf  13379  fzass4  13516  elfzomelpfzo  13727  modid  13855  swrdccatin2  14691  pfxccatin12  14695  cshwleneq  14779  s2eq2seq  14899  tanaddlem  16133  fpwipodrs  18506  gsumsgrpccat  18808  issubg4  19121  ghmpreima  19213  cntzsubg  19314  symgfixf1  19412  rnghmsubcsetclem2  20609  rhmsubcsetclem2  20638  rhmsubcrngclem2  20644  islmodd  20861  lssvsubcl  20939  lssvscl  20950  lmhmf1o  21041  pwsdiaglmhm  21052  lmimco  21824  scmatghm  22498  scmatmhm  22499  mat2pmatscmxcl  22705  fctop  22969  cctop  22971  opnneissb  23079  pnrmopn  23308  hausnei2  23318  neitx  23572  txcnmpt  23589  txrest  23596  tx1stc  23615  fbssfi  23802  opnfbas  23807  rnelfmlem  23917  alexsubALTlem3  24014  metcnp3  24505  cncfmet  24876  evth  24926  caucfil  25250  ovolun  25466  dveflem  25946  efnnfsumcl  27066  efchtdvds  27122  lgsdir2  27293  precsexlem11  28209  axdimuniq  28982  axcontlem2  29034  clwwlkf1  30119  frgrwopreglem5lem  30390  frgrwopreglem5ALT  30392  friendship  30469  hvsub4  31108  his35  31159  shscli  31388  5oalem2  31726  3oalem2  31734  hosub4  31884  hmops  32091  hmopm  32092  hmopco  32094  adjmul  32163  adjadd  32164  mdslmd1lem1  32396  mdslmd1lem2  32397  noinfepfnregs  35276  satffunlem  35583  elmrsubrn  35702  dfon2lem6  35968  funline  36324  neibastop2lem  36542  isbasisrelowllem1  37671  isbasisrelowllem2  37672  mbfposadd  37988  itg2addnc  37995  fdc  38066  seqpo  38068  ismtyval  38121  paddss12  40265  zaddcom  42909  zmulcom  42913  mzpcompact2lem  43183  jm2.26  43430  orddif0suc  43696  tfsconcatun  43765  oaun3lem2  43803  fmtnofac2lem  48031  isubgrgrim  48405  zlmodzxzsubm  48835  ltsubaddb  48990  ltsubsubb  48991