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

Theorem ad2ant2lr 747
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 716 . 2 ((𝜑 ∧ (𝜓𝜏)) → 𝜒)
32adantll 713 1 (((𝜃𝜑) ∧ (𝜓𝜏)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  mpteqb  6768  omxpenlem  8605  fineqvlem  8720  marypha1lem  8885  fin23lem26  9740  axdc3lem4  9868  mulcmpblnr  10486  ltsrpr  10492  sub4  10924  muladd  11065  ltleadd  11116  divdivdiv  11334  divadddiv  11348  ltmul12a  11489  lt2mul2div  11511  xlemul1a  12673  fzrev  12969  facndiv  13648  fsumconst  15140  fprodconst  15327  isprm5  16044  acsfn2  16929  ghmeql  18376  subgdmdprd  19152  lssvsubcl  19711  lssvacl  19722  ocvin  20366  lindfmm  20519  scmatghm  21141  scmatmhm  21142  slesolinv  21288  slesolinvbi  21289  slesolex  21290  pm2mpf1lem  21402  pm2mpcoe1  21408  reftr  22122  alexsubALTlem2  22656  alexsubALTlem3  22657  blbas  23040  nmoco  23346  cncfmet  23517  cmetcaulem  23895  mbflimsup  24273  ulmdvlem3  25000  ptolemy  25092  3wlkdlem6  27953  vdn0conngrumgrv2  27984  frgrncvvdeqlem8  28094  frgrwopreglem5ALT  28110  grpoideu  28295  ipblnfi  28641  htthlem  28703  hvaddsub4  28864  bralnfn  29734  hmops  29806  hmopm  29807  adjadd  29879  opsqrlem1  29926  atomli  30168  chirredlem2  30177  atcvat3i  30182  mdsymlem5  30193  cdj1i  30219  derangenlem  32526  elmrsubrn  32875  dfon2lem6  33141  poseq  33203  sltsolem1  33288  pibt2  34829  matunitlindflem1  35046  mblfinlem1  35087  prdsbnd  35224  heibor1lem  35240  hl2at  36694  congneg  39897  jm2.26  39930  stoweidlem34  42663  fmtnofac2lem  44072  lindslinindsimp2  44859  ltsubaddb  44910  ltsubadd2b  44912  aacllem  45316
  Copyright terms: Public domain W3C validator