Theorem ad2ant2lr 745

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

Syntax hints:   → wi 4   ∧ wa 384

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

This theorem is referenced by:  mpteqb  6530  omxpenlem  8310  fineqvlem  8423  marypha1lem  8588  fin23lem26  9442  axdc3lem4  9570  mulcmpblnr  10187  ltsrpr  10193  sub4  10621  muladd  10757  ltleadd  10806  divdivdiv  11021  divadddiv  11035  ltmul12a  11174  lt2mul2div  11196  xlemul1a  12356  fzrev  12646  facndiv  13315  fsumconst  14764  fprodconst  14949  isprm5  15656  acsfn2  16548  ghmeql  17905  subgdmdprd  18655  lssvsubcl  19168  lssvacl  19181  ocvin  20249  lindfmm  20397  scmatghm  20571  scmatmhm  20572  slesolinv  20719  slesolinvbi  20720  slesolex  20721  pm2mpf1lem  20833  pm2mpcoe1  20839  reftr  21552  alexsubALTlem2  22086  alexsubALTlem3  22087  blbas  22469  nmoco  22775  cncfmet  22945  cmetcaulem  23320  mbflimsup  23670  ulmdvlem3  24393  ptolemy  24486  3wlkdlem6  27361  vdn0conngrumgrv2  27392  frgrncvvdeqlem8  27504  frgrwopreglem5ALT  27520  grpoideu  27715  ipblnfi  28062  htthlem  28125  hvaddsub4  28286  bralnfn  29158  hmops  29230  hmopm  29231  adjadd  29303  opsqrlem1  29350  atomli  29592  chirredlem2  29601  atcvat3i  29606  mdsymlem5  29617  cdj1i  29643  derangenlem  31498  elmrsubrn  31762  dfon2lem6  32035  poseq  32096  sltsolem1  32169  matunitlindflem1  33737  mblfinlem1  33778  prdsbnd  33922  heibor1lem  33938  hl2at  35204  congneg  38055  jm2.26  38088  stoweidlem34  40748  fmtnofac2lem  42073  lindslinindsimp2  42838  ltsubaddb  42890  ltsubadd2b  42892  aacllem  43136