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  6580  mpteqb  6987  soxp  8108  oaass  8525  nadd42  8663  naddel12  8664  undifixp  8907  xpdom2  9036  tcrank  9837  inawinalem  10642  addcanpr  10999  ltsosr  11047  1re  11174  add42  11396  muladd  11610  mulsub  11621  divmuleq  11887  ltmul12a  12038  lemul12b  12039  lemul12a  12040  mulge0b  12053  qaddcl  12924  qmulcl  12926  iooshf  13387  fzass4  13523  elfzomelpfzo  13732  modid  13858  swrdccatin2  14694  pfxccatin12  14698  cshwleneq  14782  s2eq2seq  14903  tanaddlem  16134  fpwipodrs  18499  gsumsgrpccat  18767  issubg4  19077  ghmpreima  19170  cntzsubg  19271  symgfixf1  19367  rnghmsubcsetclem2  20541  rhmsubcsetclem2  20570  rhmsubcrngclem2  20576  islmodd  20772  lssvsubcl  20850  lssvscl  20861  lmhmf1o  20953  pwsdiaglmhm  20964  lmimco  21753  scmatghm  22420  scmatmhm  22421  mat2pmatscmxcl  22627  fctop  22891  cctop  22893  opnneissb  23001  pnrmopn  23230  hausnei2  23240  neitx  23494  txcnmpt  23511  txrest  23518  tx1stc  23537  fbssfi  23724  opnfbas  23729  rnelfmlem  23839  alexsubALTlem3  23936  metcnp3  24428  cncfmet  24802  evth  24858  caucfil  25183  ovolun  25400  dveflem  25883  efnnfsumcl  27013  efchtdvds  27069  lgsdir2  27241  precsexlem11  28119  axdimuniq  28840  axcontlem2  28892  clwwlkf1  29978  frgrwopreglem5lem  30249  frgrwopreglem5ALT  30251  friendship  30328  hvsub4  30966  his35  31017  shscli  31246  5oalem2  31584  3oalem2  31592  hosub4  31742  hmops  31949  hmopm  31950  hmopco  31952  adjmul  32021  adjadd  32022  mdslmd1lem1  32254  mdslmd1lem2  32255  satffunlem  35388  elmrsubrn  35507  dfon2lem6  35776  funline  36130  neibastop2lem  36348  isbasisrelowllem1  37343  isbasisrelowllem2  37344  mbfposadd  37661  itg2addnc  37668  fdc  37739  seqpo  37741  ismtyval  37794  paddss12  39813  zaddcom  42452  zmulcom  42456  mzpcompact2lem  42739  jm2.26  42991  orddif0suc  43257  tfsconcatun  43326  oaun3lem2  43364  fmtnofac2lem  47569  isubgrgrim  47929  zlmodzxzsubm  48347  ltsubaddb  48503  ltsubsubb  48504