Theorem ad2ant2l 756

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  funcnvqp  6585  mpteqb  6995  soxp  8109  oaass  8530  nadd42  8670  naddel12  8671  undifixp  8916  xpdom2  9044  tcrank  9842  inawinalem  10647  addcanpr  11004  ltsosr  11052  1re  11181  add42  11405  muladd  11619  mulsub  11630  divmuleq  11896  ltmul12a  12047  lemul12b  12048  lemul12a  12049  mulge0b  12062  qaddcl  12966  qmulcl  12968  iooshf  13430  fzass4  13567  elfzomelpfzo  13778  modid  13906  swrdccatin2  14742  pfxccatin12  14746  cshwleneq  14830  s2eq2seq  14950  tanaddlem  16198  fpwipodrs  18572  gsumsgrpccat  18874  issubg4  19187  ghmpreima  19278  cntzsubg  19379  symgfixf1  19477  rnghmsubcsetclem2  20682  rhmsubcsetclem2  20711  rhmsubcrngclem2  20717  islmodd  20933  lssvsubcl  21011  lssvscl  21022  lmhmf1o  21113  pwsdiaglmhm  21124  lmimco  21896  scmatghm  22593  scmatmhm  22594  mat2pmatscmxcl  22800  fctop  23064  cctop  23066  opnneissb  23174  pnrmopn  23403  hausnei2  23413  neitx  23667  txcnmpt  23684  txrest  23691  tx1stc  23710  fbssfi  23897  opnfbas  23902  rnelfmlem  24012  alexsubALTlem3  24109  metcnp3  24600  cncfmet  24971  evth  25021  caucfil  25345  ovolun  25561  dveflem  26041  efnnfsumcl  27167  efchtdvds  27223  lgsdir2  27394  precsexlem11  28310  axdimuniq  29114  axcontlem2  29166  clwwlkf1  30251  frgrwopreglem5lem  30522  frgrwopreglem5ALT  30524  friendship  30601  hvsub4  31240  his35  31291  shscli  31520  5oalem2  31858  3oalem2  31866  hosub4  32016  hmops  32223  hmopm  32224  hmopco  32226  adjmul  32295  adjadd  32296  mdslmd1lem1  32528  mdslmd1lem2  32529  noinfepfnregs  35428  satffunlem  35751  elmrsubrn  35870  dfon2lem6  36136  funline  36492  nmulprop  36540  neibastop2lem  36720  isbasisrelowllem1  37849  isbasisrelowllem2  37850  mbfposadd  38166  itg2addnc  38173  fdc  38244  seqpo  38246  ismtyval  38299  paddss12  40443  zaddcom  43086  zmulcom  43090  mzpcompact2lem  43332  jm2.26  43579  orddif0suc  43845  tfsconcatun  43914  oaun3lem2  43952  fmtnofac2lem  48177  isubgrgrim  48551  zlmodzxzsubm  48981  ltsubaddb  49136  ltsubsubb  49137