Theorem ad2ant2l 752

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  funcnvqp  6549  mpteqb  6955  soxp  8069  oaass  8486  nadd42  8625  naddel12  8626  undifixp  8872  xpdom2  9000  tcrank  9799  inawinalem  10603  addcanpr  10960  ltsosr  11008  1re  11135  add42  11359  muladd  11573  mulsub  11584  divmuleq  11851  ltmul12a  12002  lemul12b  12003  lemul12a  12004  mulge0b  12017  qaddcl  12906  qmulcl  12908  iooshf  13370  fzass4  13507  elfzomelpfzo  13718  modid  13846  swrdccatin2  14682  pfxccatin12  14686  cshwleneq  14770  s2eq2seq  14890  tanaddlem  16124  fpwipodrs  18497  gsumsgrpccat  18799  issubg4  19112  ghmpreima  19204  cntzsubg  19305  symgfixf1  19403  rnghmsubcsetclem2  20604  rhmsubcsetclem2  20633  rhmsubcrngclem2  20639  islmodd  20856  lssvsubcl  20934  lssvscl  20945  lmhmf1o  21036  pwsdiaglmhm  21047  lmimco  21819  scmatghm  22516  scmatmhm  22517  mat2pmatscmxcl  22723  fctop  22987  cctop  22989  opnneissb  23097  pnrmopn  23326  hausnei2  23336  neitx  23590  txcnmpt  23607  txrest  23614  tx1stc  23633  fbssfi  23820  opnfbas  23825  rnelfmlem  23935  alexsubALTlem3  24032  metcnp3  24523  cncfmet  24894  evth  24944  caucfil  25268  ovolun  25484  dveflem  25964  efnnfsumcl  27084  efchtdvds  27140  lgsdir2  27311  precsexlem11  28227  axdimuniq  29000  axcontlem2  29052  clwwlkf1  30137  frgrwopreglem5lem  30408  frgrwopreglem5ALT  30410  friendship  30487  hvsub4  31126  his35  31177  shscli  31406  5oalem2  31744  3oalem2  31752  hosub4  31902  hmops  32109  hmopm  32110  hmopco  32112  adjmul  32181  adjadd  32182  mdslmd1lem1  32414  mdslmd1lem2  32415  noinfepfnregs  35313  satffunlem  35629  elmrsubrn  35748  dfon2lem6  36014  funline  36370  neibastop2lem  36588  isbasisrelowllem1  37717  isbasisrelowllem2  37718  mbfposadd  38034  itg2addnc  38041  fdc  38112  seqpo  38114  ismtyval  38167  paddss12  40311  zaddcom  42954  zmulcom  42958  mzpcompact2lem  43200  jm2.26  43447  orddif0suc  43713  tfsconcatun  43782  oaun3lem2  43820  fmtnofac2lem  48046  isubgrgrim  48420  zlmodzxzsubm  48850  ltsubaddb  49005  ltsubsubb  49006