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  6631  mpteqb  7034  soxp  8152  wfrlem4OLD  8350  oaass  8597  nadd42  8735  naddel12  8736  undifixp  8972  undomOLD  9098  xpdom2  9105  tcrank  9921  inawinalem  10726  addcanpr  11083  ltsosr  11131  1re  11258  add42  11480  muladd  11692  mulsub  11703  divmuleq  11969  ltmul12a  12120  lemul12b  12121  lemul12a  12122  mulge0b  12135  qaddcl  13004  qmulcl  13006  iooshf  13462  fzass4  13598  elfzomelpfzo  13806  modid  13932  swrdccatin2  14763  pfxccatin12  14767  cshwleneq  14851  s2eq2seq  14972  tanaddlem  16198  fpwipodrs  18597  gsumsgrpccat  18865  issubg4  19175  ghmpreima  19268  cntzsubg  19369  symgfixf1  19469  rnghmsubcsetclem2  20648  rhmsubcsetclem2  20677  rhmsubcrngclem2  20683  islmodd  20880  lssvsubcl  20959  lssvscl  20970  lmhmf1o  21062  pwsdiaglmhm  21073  lmimco  21881  scmatghm  22554  scmatmhm  22555  mat2pmatscmxcl  22761  fctop  23026  cctop  23028  opnneissb  23137  pnrmopn  23366  hausnei2  23376  neitx  23630  txcnmpt  23647  txrest  23654  tx1stc  23673  fbssfi  23860  opnfbas  23865  rnelfmlem  23975  alexsubALTlem3  24072  metcnp3  24568  cncfmet  24948  evth  25004  caucfil  25330  ovolun  25547  dveflem  26031  efnnfsumcl  27160  efchtdvds  27216  lgsdir2  27388  precsexlem11  28255  axdimuniq  28942  axcontlem2  28994  clwwlkf1  30077  frgrwopreglem5lem  30348  frgrwopreglem5ALT  30350  friendship  30427  hvsub4  31065  his35  31116  shscli  31345  5oalem2  31683  3oalem2  31691  hosub4  31841  hmops  32048  hmopm  32049  hmopco  32051  adjmul  32120  adjadd  32121  mdslmd1lem1  32353  mdslmd1lem2  32354  satffunlem  35385  elmrsubrn  35504  dfon2lem6  35769  funline  36123  neibastop2lem  36342  isbasisrelowllem1  37337  isbasisrelowllem2  37338  mbfposadd  37653  itg2addnc  37660  fdc  37731  seqpo  37733  ismtyval  37786  paddss12  39801  zaddcom  42458  zmulcom  42462  mzpcompact2lem  42738  jm2.26  42990  orddif0suc  43257  tfsconcatun  43326  oaun3lem2  43364  fmtnofac2lem  47492  isubgrgrim  47834  zlmodzxzsubm  48203  ltsubaddb  48359  ltsubsubb  48360