Theorem ad2ant2l 758

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 728	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒)
3	2	adantll 726	1 ⊢ (((𝜃 ∧ 𝜑) ∧ (𝜏 ∧ 𝜓)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  funcnvqp  6601  mpteqb  7010  soxp  8125  oaass  8546  nadd42  8686  naddel12  8687  undifixp  8932  xpdom2  9060  tcrank  9856  inawinalem  10674  addcanpr  11031  ltsosr  11079  1re  11208  add42  11432  muladd  11646  mulsub  11657  divmuleq  11920  ltmul12a  12071  lemul12b  12072  lemul12a  12073  mulge0b  12085  qaddcl  12989  qmulcl  12991  iooshf  13453  fzass4  13590  elfzomelpfzo  13801  modid  13929  swrdccatin2  14766  pfxccatin12  14770  cshwleneq  14854  s2eq2seq  14974  tanaddlem  16222  fpwipodrs  18596  gsumsgrpccat  18899  issubg4  19212  ghmpreima  19308  cntzsubg  19409  symgfixf1  19507  rnghmsubcsetclem2  20717  rhmsubcsetclem2  20746  rhmsubcrngclem2  20752  islmodd  20965  lssvsubcl  21043  lssvscl  21054  lmhmf1o  21145  pwsdiaglmhm  21156  lmimco  21963  scmatghm  22659  scmatmhm  22660  mat2pmatscmxcl  22866  fctop  23130  cctop  23132  opnneissb  23240  pnrmopn  23469  hausnei2  23479  neitx  23733  txcnmpt  23750  txrest  23757  tx1stc  23776  fbssfi  23963  opnfbas  23968  rnelfmlem  24078  alexsubALTlem3  24175  metcnp3  24666  cncfmet  25037  evth  25087  caucfil  25411  ovolun  25627  dveflem  26107  efnnfsumcl  27233  efchtdvds  27289  lgsdir2  27460  precsexlem11  28376  axdimuniq  29204  axcontlem2  29256  clwwlkf1  30341  frgrwopreglem5lem  30612  frgrwopreglem5ALT  30614  friendship  30691  hvsub4  31330  his35  31381  shscli  31610  5oalem2  31948  3oalem2  31956  hosub4  32106  hmops  32313  hmopm  32314  hmopco  32316  adjmul  32385  adjadd  32386  mdslmd1lem1  32618  mdslmd1lem2  32619  noinfepfnregs  35468  satffunlem  35792  elmrsubrn  35911  dfon2lem6  36177  funline  36533  nmulprop  36581  neibastop2lem  36760  isbasisrelowllem1  37889  isbasisrelowllem2  37890  mbfposadd  38206  itg2addnc  38213  fdc  38284  seqpo  38286  ismtyval  38339  paddss12  40483  zaddcom  43128  zmulcom  43132  mzpcompact2lem  43374  jm2.26  43621  orddif0suc  43887  tfsconcatun  43956  oaun3lem2  43994  fmtnofac2lem  48209  isubgrgrim  48583  zlmodzxzsubm  49024  ltsubaddb  49179  ltsubsubb  49180