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

Theorem ad2ant2rl 780
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 24-Nov-2007.)
Hypothesis
Ref Expression
ad2ant2.1 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
ad2ant2rl (((𝜑𝜃) ∧ (𝜏𝜓)) → 𝜒)

Proof of Theorem ad2ant2rl
StepHypRef Expression
1 ad2ant2.1 . . 3 ((𝜑𝜓) → 𝜒)
21adantrl 747 . 2 ((𝜑 ∧ (𝜏𝜓)) → 𝜒)
32adantlr 746 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:  omwordri  7516  omxpenlem  7923  infxpabs  8894  domfin4  8993  isf32lem7  9041  ordpipq  9620  muladd  10313  lemul12b  10731  mulge0b  10744  qaddcl  11638  iooshf  12081  elfzomelpfzo  12395  expnegz  12713  bitsshft  14983  setscom  15679  catideu  16107  lubun  16894  grplmulf1o  17260  lmodfopne  18672  lidl1el  18987  frlmipval  19884  en2top  20547  cnpnei  20825  kgenidm  21107  ufileu  21480  fmfnfmlem4  21518  isngp4  22173  fsumcn  22428  evth  22513  mbfmulc2lem  23164  itg1addlem4  23216  dgreq0  23769  cxplt3  24190  cxple3  24191  basellem4  24554  axcontlem2  25590  usgra2adedgspth  25934  usghashecclwwlk  26155  grpoidinvlem3  26537  grpoideu  26540  grporcan  26549  3oalem2  27699  hmops  28056  adjadd  28129  mdslmd4i  28369  mdexchi  28371  mdsymlem1  28439  bnj607  30033  cvxscon  30272  poseq  30787  sltsolem1  30860  nodenselem5  30877  tailfb  31335  poimirlem14  32376  mblfinlem4  32402  ismblfin  32403  ismtyres  32560  ghomco  32643  rngoisocnv  32733  1idl  32778  ps-2  33565  umgr2edg  40417  nbumgrvtx  40549  umgrhashecclwwlk  41243  av-numclwwlk7lem  41524  srhmsubc  41849  srhmsubcALTV  41868  aacllem  42298
  Copyright terms: Public domain W3C validator