Theorem ad2ant2l 759

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  funcnvqp  6604  mpteqb  7013  soxp  8131  oaass  8552  nadd42  8692  naddel12  8693  undifixp  8938  xpdom2  9067  tcrank  9863  inawinalem  10691  addcanpr  11048  ltsosr  11096  1re  11225  add42  11449  muladd  11663  mulsub  11674  divmuleq  11937  ltmul12a  12088  lemul12b  12089  lemul12a  12090  mulge0b  12102  qaddcl  13007  qmulcl  13009  iooshf  13471  fzass4  13609  elfzomelpfzo  13820  modid  13949  swrdccatin2  14790  pfxccatin12  14794  cshwleneq  14880  s2eq2seq  15000  tanaddlem  16246  fpwipodrs  18620  gsumsgrpccat  18938  issubg4  19258  ghmpreima  19354  cntzsubg  19455  symgfixf1  19553  rnghmsubcsetclem2  20783  rhmsubcsetclem2  20812  rhmsubcrngclem2  20818  islmodd  21039  lssvsubcl  21117  lssvscl  21128  lmhmf1o  21219  pwsdiaglmhm  21230  lmimco  22046  scmatghm  22742  scmatmhm  22743  mat2pmatscmxcl  22949  fctop  23213  cctop  23215  opnneissb  23323  pnrmopn  23552  hausnei2  23562  neitx  23817  txcnmpt  23834  txrest  23841  tx1stc  23860  fbssfi  24047  opnfbas  24052  rnelfmlem  24162  alexsubALTlem3  24259  metcnp3  24750  cncfmet  25121  evth  25171  caucfil  25495  ovolun  25711  dveflem  26191  efnnfsumcl  27320  efchtdvds  27376  lgsdir2  27547  precsexlem11  28463  axdimuniq  29320  axcontlem2  29372  clwwlkf1  30469  frgrwopreglem5lem  30744  frgrwopreglem5ALT  30746  friendship  30823  hvsub4  31462  his35  31513  shscli  31742  5oalem2  32080  3oalem2  32088  hosub4  32238  hmops  32445  hmopm  32446  hmopco  32448  adjmul  32517  adjadd  32518  mdslmd1lem1  32750  mdslmd1lem2  32751  noinfepfnregs  35604  satffunlem  35932  elmrsubrn  36051  dfon2lem6  36317  funline  36673  nmulprop  36721  nmulel1  36746  neibastop2lem  36930  isbasisrelowllem1  38060  isbasisrelowllem2  38061  mbfposadd  38377  itg2addnc  38384  fdc  38456  seqpo  38458  ismtyval  38511  paddss12  40653  zaddcom  43298  zmulcom  43302  mzpcompact2lem  43542  jm2.26  43789  orddif0suc  44055  tfsconcatun  44124  oaun3lem2  44162  fmtnofac2lem  48380  isubgrgrim  48754  zlmodzxzsubm  49198  ltsubaddb  49353  ltsubsubb  49354