Theorem ad2ant2l 778

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  funcnvqp  5866  mpteqb  6207  mpt2fun  6660  soxp  7177  wfrlem4  7305  oaass  7528  undifixp  7830  undom  7933  xpdom2  7940  tcrank  8630  inawinalem  9390  addcanpr  9747  ltsosr  9794  1re  9918  add42  10136  muladd  10341  mulsub  10352  divmuleq  10609  ltmul12a  10758  lemul12b  10759  lemul12a  10760  mulge0b  10772  qaddcl  11680  qmulcl  11682  iooshf  12123  fzass4  12250  elfzomelpfzo  12438  modid  12557  cshwleneq  13414  s2eq2seq  13532  tanaddlem  14735  fpwipodrs  16987  issubg4  17436  ghmpreima  17505  cntzsubg  17592  symgfixf1  17680  islmodd  18692  lssvsubcl  18765  lssvscl  18776  lmhmf1o  18867  pwsdiaglmhm  18878  lmimco  20002  scmatghm  20158  scmatmhm  20159  mat2pmatscmxcl  20364  fctop  20618  cctop  20620  opnneissb  20728  pnrmopn  20957  hausnei2  20967  neitx  21220  txcnmpt  21237  txrest  21244  tx1stc  21263  fbssfi  21451  opnfbas  21456  rnelfmlem  21566  alexsubALTlem3  21663  metcnp3  22155  cncfmet  22519  evth  22566  caucfil  22889  ovolun  23074  dveflem  23546  efnnfsumcl  24629  efchtdvds  24685  lgsdir2  24855  axdimuniq  25593  axcontlem2  25645  friendship  26649  hvsub4  27278  his35  27329  shscli  27560  5oalem2  27898  3oalem2  27906  hosub4  28056  hmops  28263  hmopm  28264  hmopco  28266  adjmul  28335  adjadd  28336  mdslmd1lem1  28568  mdslmd1lem2  28569  elmrsubrn  30671  dfon2lem6  30937  nofulllem4  31104  funline  31419  neibastop2lem  31525  isbasisrelowllem1  32379  isbasisrelowllem2  32380  mbfposadd  32627  itg2addnc  32634  fdc  32711  seqpo  32713  ismtyval  32769  paddss12  34123  mzpcompact2lem  36332  jm2.26  36587  fmtnofac2lem  40018  av-friendship  41553  rnghmsubcsetclem2  41768  rhmsubcsetclem2  41814  rhmsubcrngclem2  41820  zlmodzxzsubm  41930  ltsubaddb  42098  ltsubsubb  42099