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  6612  mpteqb  7021  soxp  8151  oaass  8580  nadd42  8720  naddel12  8721  undifixp  8973  xpdom2  9102  tcrank  9911  elhf3OLD  9933  inawinalem  10784  addcanpr  11141  ltsosr  11189  1re  11318  add42  11542  muladd  11758  mulsub  11769  divmuleq  12032  ltmul12a  12183  lemul12b  12184  lemul12a  12185  mulge0b  12197  qaddcl  13103  qmulcl  13105  iooshf  13567  fzass4  13706  elfzomelpfzo  13917  modid  14046  swrdccatin2  14889  pfxccatin12  14893  cshwleneq  14979  s2eq2seq  15100  tanaddlem  16346  fpwipodrs  18726  gsumsgrpccat  19048  issubg4  19368  ghmpreima  19464  cntzsubg  19565  symgfixf1  19663  rnghmsubcsetclem2  20896  rhmsubcsetclem2  20925  rhmsubcrngclem2  20931  islmodd  21153  lssvsubcl  21231  lssvscl  21242  lmhmf1o  21333  pwsdiaglmhm  21344  lmimco  22162  scmatghm  22860  scmatmhm  22861  mat2pmatscmxcl  23070  fctop  23334  cctop  23336  opnneissb  23444  pnrmopn  23673  hausnei2  23683  neitx  23938  txcnmpt  23955  txrest  23962  tx1stc  23981  fbssfi  24168  opnfbas  24173  rnelfmlem  24283  alexsubALTlem3  24380  metcnp3  24871  cncfmet  25242  evth  25292  caucfil  25616  ovolun  25832  dveflem  26311  efnnfsumcl  27442  efchtdvds  27498  lgsdir2  27669  precsexlem11  28615  axdimuniq  29503  axcontlem2  29555  clwwlkf1  30652  frgrwopreglem5lem  30933  frgrwopreglem5ALT  30935  friendship  31012  hvsub4  31651  his35  31702  shscli  31931  5oalem2  32269  3oalem2  32277  hosub4  32427  hmops  32634  hmopm  32635  hmopco  32637  adjmul  32706  adjadd  32707  mdslmd1lem1  32939  mdslmd1lem2  32940  noinfepfnregs  35871  satffunlem  36287  elmrsubrn  36406  dfon2lem6  36677  funline  37034  nmulprop  37066  nmulel1  37091  neibastop2lem  37275  isbasisrelowllem1  38418  isbasisrelowllem2  38419  mbfposadd  38725  itg2addnc  38732  fdc  38819  seqpo  38821  ismtyval  38874  paddss12  41016  zaddcom  43668  zmulcom  43672  mzpcompact2lem  43902  jm2.26  44149  orddif0suc  44410  tfsconcatun  44479  oaun3lem2  44517  fmtnofac2lem  48792  isubgrgrim  49166  zlmodzxzsubm  49610  ltsubaddb  49765  ltsubsubb  49766