Theorem ad2ant2lr 749

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 718	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒)
3	2	adantll 715	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:  mpteqb  6969  poseq  8110  omxpenlem  9018  fineqvlem  9178  marypha1lem  9348  fin23lem26  10247  axdc3lem4  10375  mulcmpblnr  10994  ltsrpr  11000  sub4  11438  muladd  11581  ltleadd  11632  divdivdiv  11854  divadddiv  11868  ltmul12a  12009  lt2mul2div  12032  xlemul1a  13215  fzrev  13515  facndiv  14223  fsumconst  15725  fprodconst  15913  isprm5  16646  acsfn2  17598  ghmeql  19180  subgdmdprd  19977  lssvacl  20906  lssvsubcl  20907  ocvin  21641  lindfmm  21794  sraassab  21835  scmatghm  22489  scmatmhm  22490  slesolinv  22636  slesolinvbi  22637  slesolex  22638  pm2mpf1lem  22750  pm2mpcoe1  22756  reftr  23470  alexsubALTlem2  24004  alexsubALTlem3  24005  blbas  24386  nmoco  24693  cncfmet  24870  cmetcaulem  25256  mbflimsup  25635  ulmdvlem3  26379  ptolemy  26473  ltssolem1  27655  madebdaylemlrcut  27907  3wlkdlem6  30252  vdn0conngrumgrv2  30283  frgrncvvdeqlem8  30393  frgrwopreglem5ALT  30409  grpoideu  30596  ipblnfi  30942  htthlem  31004  hvaddsub4  31165  bralnfn  32035  hmops  32107  hmopm  32108  adjadd  32180  opsqrlem1  32227  atomli  32469  chirredlem2  32478  atcvat3i  32483  mdsymlem5  32494  cdj1i  32520  derangenlem  35384  elmrsubrn  35733  dfon2lem6  35999  pibt2  37669  matunitlindflem1  37864  mblfinlem1  37905  prdsbnd  38041  heibor1lem  38057  hl2at  39778  congneg  43323  jm2.26  43356  stoweidlem34  46389  fmtnofac2lem  47925  lindslinindsimp2  48820  ltsubaddb  48871  ltsubadd2b  48873  aacllem  50157