Theorem ad2ant2lr 746

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 23-Nov-2007.)

Hypothesis

Ref	Expression
ad2ant2.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
ad2ant2lr	⊢ (((𝜃 ∧ 𝜑) ∧ (𝜓 ∧ 𝜏)) → 𝜒)

Proof of Theorem ad2ant2lr

Step	Hyp	Ref	Expression
1		ad2ant2.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantrr 715	. 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:  mpteqb  7017  poseq  8143  omxpenlem  9072  fineqvlem  9261  marypha1lem  9427  fin23lem26  10319  axdc3lem4  10447  mulcmpblnr  11065  ltsrpr  11071  sub4  11504  muladd  11645  ltleadd  11696  divdivdiv  11914  divadddiv  11928  ltmul12a  12069  lt2mul2div  12091  xlemul1a  13266  fzrev  13563  facndiv  14247  fsumconst  15735  fprodconst  15921  isprm5  16643  acsfn2  17606  ghmeql  19114  subgdmdprd  19903  lssvsubcl  20553  lssvacl  20564  ocvin  21226  lindfmm  21381  sraassab  21421  scmatghm  22034  scmatmhm  22035  slesolinv  22181  slesolinvbi  22182  slesolex  22183  pm2mpf1lem  22295  pm2mpcoe1  22301  reftr  23017  alexsubALTlem2  23551  alexsubALTlem3  23552  blbas  23935  nmoco  24253  cncfmet  24424  cmetcaulem  24804  mbflimsup  25182  ulmdvlem3  25913  ptolemy  26005  sltsolem1  27175  madebdaylemlrcut  27390  3wlkdlem6  29415  vdn0conngrumgrv2  29446  frgrncvvdeqlem8  29556  frgrwopreglem5ALT  29572  grpoideu  29757  ipblnfi  30103  htthlem  30165  hvaddsub4  30326  bralnfn  31196  hmops  31268  hmopm  31269  adjadd  31341  opsqrlem1  31388  atomli  31630  chirredlem2  31639  atcvat3i  31644  mdsymlem5  31655  cdj1i  31681  derangenlem  34157  elmrsubrn  34506  dfon2lem6  34755  pibt2  36293  matunitlindflem1  36479  mblfinlem1  36520  prdsbnd  36656  heibor1lem  36672  hl2at  38271  congneg  41698  jm2.26  41731  stoweidlem34  44740  fmtnofac2lem  46226  lindslinindsimp2  47134  ltsubaddb  47185  ltsubadd2b  47187  aacllem  47838