MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ad2ant2lr Structured version   Visualization version   GIF version

Theorem ad2ant2lr 780
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
StepHypRef Expression
1 ad2ant2.1 . . 3 ((𝜑𝜓) → 𝜒)
21adantrr 749 . 2 ((𝜑 ∧ (𝜓𝜏)) → 𝜒)
32adantll 746 1 (((𝜃𝜑) ∧ (𝜓𝜏)) → 𝜒)
Colors of variables: wff setvar class
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:  reusv2lem2OLD  4796  mpteqb  6207  omxpenlem  7946  fineqvlem  8059  marypha1lem  8222  fin23lem26  9030  axdc3lem4  9158  mulcmpblnr  9771  ltsrpr  9777  sub4  10205  muladd  10341  ltleadd  10390  divdivdiv  10605  divadddiv  10619  ltmul12a  10758  lt2mul2div  10780  xlemul1a  11990  fzrev  12273  facndiv  12937  fsumconst  14364  fprodconst  14547  isprm5  15257  acsfn2  16147  ghmeql  17506  subgdmdprd  18256  lssvsubcl  18765  lssvacl  18775  ocvin  19837  lindfmm  19985  scmatghm  20158  scmatmhm  20159  slesolinv  20305  slesolinvbi  20306  slesolex  20307  pm2mpf1lem  20418  pm2mpcoe1  20424  reftr  21127  alexsubALTlem2  21662  alexsubALTlem3  21663  blbas  22045  nmoco  22351  cncfmet  22519  cmetcaulem  22894  mbflimsup  23239  ulmdvlem3  23960  ptolemy  24052  grpoideu  26747  ipblnfi  27095  htthlem  27158  hvaddsub4  27319  bralnfn  28191  hmops  28263  hmopm  28264  adjadd  28336  opsqrlem1  28383  atomli  28625  chirredlem2  28634  atcvat3i  28639  mdsymlem5  28650  cdj1i  28676  derangenlem  30407  elmrsubrn  30671  dfon2lem6  30937  poseq  30994  sltsolem1  31067  matunitlindflem1  32575  mblfinlem1  32616  prdsbnd  32762  heibor1lem  32778  hl2at  33709  congneg  36554  jm2.26  36587  stoweidlem34  38927  fmtnofac2lem  40018  31wlkdlem6  41332  vdn0conngrumgrv2  41363  lindslinindsimp2  42046  ltsubaddb  42098  ltsubadd2b  42100  aacllem  42356
  Copyright terms: Public domain W3C validator