Theorem ad2ant2l 736

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

Syntax hints:   → wi 4   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  funcnvqp  6198  mpteqb  6560  mpt2fun  7039  soxp  7571  wfrlem4  7700  wfrlem4OLD  7701  oaass  7925  undifixp  8230  undom  8336  xpdom2  8343  tcrank  9044  inawinalem  9846  addcanpr  10203  ltsosr  10251  1re  10376  add42  10597  muladd  10807  mulsub  10818  divmuleq  11080  ltmul12a  11233  lemul12b  11234  lemul12a  11235  mulge0b  11247  qaddcl  12112  qmulcl  12114  iooshf  12564  fzass4  12696  elfzomelpfzo  12891  modid  13014  cshwleneq  13968  s2eq2seq  14088  tanaddlem  15298  fpwipodrs  17550  issubg4  17997  ghmpreima  18066  cntzsubg  18152  symgfixf1  18240  islmodd  19261  lssvsubcl  19336  lssvscl  19350  lmhmf1o  19441  pwsdiaglmhm  19452  lmimco  20587  scmatghm  20744  scmatmhm  20745  mat2pmatscmxcl  20952  fctop  21216  cctop  21218  opnneissb  21326  pnrmopn  21555  hausnei2  21565  neitx  21819  txcnmpt  21836  txrest  21843  tx1stc  21862  fbssfi  22049  opnfbas  22054  rnelfmlem  22164  alexsubALTlem3  22261  metcnp3  22753  cncfmet  23119  evth  23166  caucfil  23489  ovolun  23703  dveflem  24179  efnnfsumcl  25281  efchtdvds  25337  lgsdir2  25507  axdimuniq  26262  axcontlem2  26314  clwwlkf1  27445  frgrwopreglem5lem  27728  frgrwopreglem5ALT  27730  friendship  27831  hvsub4  28466  his35  28517  shscli  28748  5oalem2  29086  3oalem2  29094  hosub4  29244  hmops  29451  hmopm  29452  hmopco  29454  adjmul  29523  adjadd  29524  mdslmd1lem1  29756  mdslmd1lem2  29757  elmrsubrn  32016  dfon2lem6  32281  funline  32838  neibastop2lem  32943  isbasisrelowllem1  33798  isbasisrelowllem2  33799  mbfposadd  34066  itg2addnc  34073  fdc  34149  seqpo  34151  ismtyval  34207  paddss12  35957  mzpcompact2lem  38256  jm2.26  38510  fmtnofac2lem  42483  rnghmsubcsetclem2  42973  rhmsubcsetclem2  43019  rhmsubcrngclem2  43025  zlmodzxzsubm  43134  ltsubaddb  43301  ltsubsubb  43302