Theorem ad2ant2l 744

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 714	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒)
3	2	adantll 712	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 206  df-an 397

This theorem is referenced by:  funcnvqp  6612  mpteqb  7017  mpofunOLD  7532  soxp  8114  wfrlem4OLD  8311  oaass  8560  nadd42  8697  naddel12  8698  undifixp  8927  undomOLD  9059  xpdom2  9066  tcrank  9878  inawinalem  10683  addcanpr  11040  ltsosr  11088  1re  11213  add42  11434  muladd  11645  mulsub  11656  divmuleq  11918  ltmul12a  12069  lemul12b  12070  lemul12a  12071  mulge0b  12083  qaddcl  12948  qmulcl  12950  iooshf  13402  fzass4  13538  elfzomelpfzo  13735  modid  13860  swrdccatin2  14678  pfxccatin12  14682  cshwleneq  14766  s2eq2seq  14887  tanaddlem  16108  fpwipodrs  18492  gsumsgrpccat  18720  issubg4  19024  ghmpreima  19113  cntzsubg  19202  symgfixf1  19304  islmodd  20476  lssvsubcl  20553  lssvscl  20565  lmhmf1o  20656  pwsdiaglmhm  20667  lmimco  21398  scmatghm  22034  scmatmhm  22035  mat2pmatscmxcl  22241  fctop  22506  cctop  22508  opnneissb  22617  pnrmopn  22846  hausnei2  22856  neitx  23110  txcnmpt  23127  txrest  23134  tx1stc  23153  fbssfi  23340  opnfbas  23345  rnelfmlem  23455  alexsubALTlem3  23552  metcnp3  24048  cncfmet  24424  evth  24474  caucfil  24799  ovolun  25015  dveflem  25495  efnnfsumcl  26604  efchtdvds  26660  lgsdir2  26830  precsexlem11  27660  axdimuniq  28168  axcontlem2  28220  clwwlkf1  29299  frgrwopreglem5lem  29570  frgrwopreglem5ALT  29572  friendship  29649  hvsub4  30285  his35  30336  shscli  30565  5oalem2  30903  3oalem2  30911  hosub4  31061  hmops  31268  hmopm  31269  hmopco  31271  adjmul  31340  adjadd  31341  mdslmd1lem1  31573  mdslmd1lem2  31574  satffunlem  34387  elmrsubrn  34506  dfon2lem6  34755  funline  35109  neibastop2lem  35240  isbasisrelowllem1  36231  isbasisrelowllem2  36232  mbfposadd  36530  itg2addnc  36537  fdc  36608  seqpo  36610  ismtyval  36663  paddss12  38685  zaddcom  41326  zmulcom  41330  mzpcompact2lem  41479  jm2.26  41731  orddif0suc  42008  tfsconcatun  42077  oaun3lem2  42115  fmtnofac2lem  46226  rnghmsubcsetclem2  46864  rhmsubcsetclem2  46910  rhmsubcrngclem2  46916  zlmodzxzsubm  47025  ltsubaddb  47185  ltsubsubb  47186