Theorem ad2ant2l 746

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 716	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒)
3	2	adantll 714	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  6546  mpteqb  6949  soxp  8062  oaass  8479  nadd42  8617  naddel12  8618  undifixp  8861  xpdom2  8989  tcrank  9780  inawinalem  10583  addcanpr  10940  ltsosr  10988  1re  11115  add42  11338  muladd  11552  mulsub  11563  divmuleq  11829  ltmul12a  11980  lemul12b  11981  lemul12a  11982  mulge0b  11995  qaddcl  12866  qmulcl  12868  iooshf  13329  fzass4  13465  elfzomelpfzo  13674  modid  13800  swrdccatin2  14635  pfxccatin12  14639  cshwleneq  14723  s2eq2seq  14844  tanaddlem  16075  fpwipodrs  18446  gsumsgrpccat  18714  issubg4  19024  ghmpreima  19117  cntzsubg  19218  symgfixf1  19316  rnghmsubcsetclem2  20517  rhmsubcsetclem2  20546  rhmsubcrngclem2  20552  islmodd  20769  lssvsubcl  20847  lssvscl  20858  lmhmf1o  20950  pwsdiaglmhm  20961  lmimco  21751  scmatghm  22418  scmatmhm  22419  mat2pmatscmxcl  22625  fctop  22889  cctop  22891  opnneissb  22999  pnrmopn  23228  hausnei2  23238  neitx  23492  txcnmpt  23509  txrest  23516  tx1stc  23535  fbssfi  23722  opnfbas  23727  rnelfmlem  23837  alexsubALTlem3  23934  metcnp3  24426  cncfmet  24800  evth  24856  caucfil  25181  ovolun  25398  dveflem  25881  efnnfsumcl  27011  efchtdvds  27067  lgsdir2  27239  precsexlem11  28124  axdimuniq  28858  axcontlem2  28910  clwwlkf1  29993  frgrwopreglem5lem  30264  frgrwopreglem5ALT  30266  friendship  30343  hvsub4  30981  his35  31032  shscli  31261  5oalem2  31599  3oalem2  31607  hosub4  31757  hmops  31964  hmopm  31965  hmopco  31967  adjmul  32036  adjadd  32037  mdslmd1lem1  32269  mdslmd1lem2  32270  satffunlem  35384  elmrsubrn  35503  dfon2lem6  35772  funline  36126  neibastop2lem  36344  isbasisrelowllem1  37339  isbasisrelowllem2  37340  mbfposadd  37657  itg2addnc  37664  fdc  37735  seqpo  37737  ismtyval  37790  paddss12  39808  zaddcom  42447  zmulcom  42451  mzpcompact2lem  42734  jm2.26  42985  orddif0suc  43251  tfsconcatun  43320  oaun3lem2  43358  fmtnofac2lem  47562  isubgrgrim  47923  zlmodzxzsubm  48353  ltsubaddb  48509  ltsubsubb  48510