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

Theorem ad2ant2rl 800
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 752 . 2 ((𝜑 ∧ (𝜏𝜓)) → 𝜒)
32adantlr 751 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 197  df-an 385
This theorem is referenced by:  omwordri  7697  omxpenlem  8102  infxpabs  9072  domfin4  9171  isf32lem7  9219  ordpipq  9802  muladd  10500  lemul12b  10918  mulge0b  10931  qaddcl  11842  iooshf  12290  elfzomelpfzo  12612  expnegz  12934  bitsshft  15244  setscom  15950  lubun  17170  grplmulf1o  17536  lmodfopne  18949  lidl1el  19266  frlmipval  20166  en2top  20837  cnpnei  21116  kgenidm  21398  ufileu  21770  fmfnfmlem4  21808  isngp4  22463  fsumcn  22720  evth  22805  mbfmulc2lem  23459  itg1addlem4  23511  dgreq0  24066  cxplt3  24491  cxple3  24492  basellem4  24855  axcontlem2  25890  umgr2edg  26146  nbumgrvtx  26287  umgrhashecclwwlk  27042  frgrncvvdeqlem9  27287  frgrwopreglem5ALT  27302  numclwwlk7lem  27376  grpoidinvlem3  27488  grpoideu  27491  grporcan  27500  3oalem2  28650  hmops  29007  adjadd  29080  mdslmd4i  29320  mdexchi  29322  mdsymlem1  29390  bnj607  31112  cvxsconn  31351  poseq  31878  sltsolem1  31951  nodenselem7  31965  tailfb  32497  poimirlem14  33553  mblfinlem4  33579  ismblfin  33580  ismtyres  33737  ghomco  33820  rngoisocnv  33910  1idl  33955  ps-2  35082  srhmsubc  42401  srhmsubcALTV  42419  aacllem  42875
  Copyright terms: Public domain W3C validator