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

Theorem ad2ant2rl 743
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 695 . 2 ((𝜑 ∧ (𝜏𝜓)) → 𝜒)
32adantlr 694 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 197  df-an 383
This theorem is referenced by:  omwordri  7806  omxpenlem  8217  infxpabs  9236  domfin4  9335  isf32lem7  9383  ordpipq  9966  muladd  10664  lemul12b  11082  mulge0b  11095  qaddcl  12008  iooshf  12453  elfzomelpfzo  12776  expnegz  13097  bitsshft  15401  setscom  16106  lubun  17327  grplmulf1o  17693  lmodfopne  19107  lidl1el  19429  frlmipval  20331  en2top  21006  cnpnei  21285  kgenidm  21567  ufileu  21939  fmfnfmlem4  21977  isngp4  22632  fsumcn  22889  evth  22974  mbfmulc2lem  23630  itg1addlem4  23682  dgreq0  24237  cxplt3  24663  cxple3  24664  basellem4  25027  axcontlem2  26062  umgr2edg  26319  nbumgrvtx  26461  umgrhashecclwwlk  27232  frgrncvvdeqlem9  27485  frgrwopreglem5ALT  27500  numclwwlk7lem  27584  grpoidinvlem3  27696  grpoideu  27699  grporcan  27708  3oalem2  28858  hmops  29215  adjadd  29288  mdslmd4i  29528  mdexchi  29530  mdsymlem1  29598  bnj607  31320  cvxsconn  31559  poseq  32086  sltsolem1  32159  nodenselem7  32173  tailfb  32705  poimirlem14  33752  mblfinlem4  33778  ismblfin  33779  ismtyres  33935  ghomco  34018  rngoisocnv  34108  1idl  34153  ps-2  35283  srhmsubc  42601  srhmsubcALTV  42619  aacllem  43075
  Copyright terms: Public domain W3C validator