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

Theorem ad2ant2lr 779
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 748 . 2 ((𝜑 ∧ (𝜓𝜏)) → 𝜒)
32adantll 745 1 (((𝜃𝜑) ∧ (𝜓𝜏)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  reusv2lem2OLD  4791  mpteqb  6192  omxpenlem  7924  fineqvlem  8037  marypha1lem  8200  fin23lem26  9008  axdc3lem4  9136  mulcmpblnr  9749  ltsrpr  9755  sub4  10178  muladd  10314  ltleadd  10363  divdivdiv  10578  divadddiv  10592  ltmul12a  10731  lt2mul2div  10753  xlemul1a  11950  fzrev  12231  facndiv  12895  fsumconst  14313  fprodconst  14496  isprm5  15206  acsfn2  16096  ghmeql  17455  subgdmdprd  18205  lssvsubcl  18714  lssvacl  18724  ocvin  19785  lindfmm  19933  scmatghm  20106  scmatmhm  20107  slesolinv  20253  slesolinvbi  20254  slesolex  20255  pm2mpf1lem  20366  pm2mpcoe1  20372  reftr  21075  alexsubALTlem2  21610  alexsubALTlem3  21611  blbas  21993  nmoco  22299  cncfmet  22467  cmetcaulem  22839  mbflimsup  23184  ulmdvlem3  23905  ptolemy  23997  grpoideu  26541  ipblnfi  26929  htthlem  26992  hvaddsub4  27153  bralnfn  28025  hmops  28097  hmopm  28098  adjadd  28170  opsqrlem1  28217  atomli  28459  chirredlem2  28468  atcvat3i  28473  mdsymlem5  28484  cdj1i  28510  derangenlem  30241  elmrsubrn  30505  dfon2lem6  30771  poseq  30828  sltsolem1  30901  matunitlindflem1  32399  mblfinlem1  32440  prdsbnd  32586  heibor1lem  32602  hl2at  33533  congneg  36378  jm2.26  36411  stoweidlem34  38751  fmtnofac2lem  39843  31wlkdlem6  41354  vdn0conngrumgrv2  41385  lindslinindsimp2  42068  ltsubaddb  42120  ltsubadd2b  42122  aacllem  42339
  Copyright terms: Public domain W3C validator