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

Theorem ad2ant2rl 748
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 715 . 2 ((𝜑 ∧ (𝜏𝜓)) → 𝜒)
32adantlr 714 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:  omwordri  8194  omxpenlem  8614  infxpabs  9632  domfin4  9731  isf32lem7  9779  ordpipq  10362  muladd  11070  lemul12b  11495  mulge0b  11508  qaddcl  12361  iooshf  12813  elfzomelpfzo  13145  expnegz  13468  swrdccatin1  14087  bitsshft  15822  setscom  16527  lubun  17733  grplmulf1o  18173  lmodfopne  19672  lidl1el  19991  frlmipval  20923  en2top  21593  cnpnei  21872  kgenidm  22155  ufileu  22527  fmfnfmlem4  22565  isngp4  23221  fsumcn  23478  evth  23567  cmslssbn  23979  mbfmulc2lem  24254  itg1addlem4  24306  dgreq0  24865  cxplt3  25294  cxple3  25295  basellem4  25672  axcontlem2  26762  umgr2edg  27002  nbumgrvtx  27139  clwwlkf1  27837  umgrhashecclwwlk  27866  frgrncvvdeqlem9  28095  frgrwopreglem5ALT  28110  numclwwlk7lem  28177  grpoidinvlem3  28292  grpoideu  28295  grporcan  28304  3oalem2  29449  hmops  29806  adjadd  29879  mdslmd4i  30119  mdexchi  30121  mdsymlem1  30189  bnj607  32245  cvxsconn  32547  poseq  33152  sltsolem1  33237  nodenselem7  33251  tailfb  33782  lindsadd  34995  poimirlem14  35016  mblfinlem4  35042  ismblfin  35043  ismtyres  35191  ghomco  35274  rngoisocnv  35364  1idl  35409  ps-2  36719  srhmsubc  44626  srhmsubcALTV  44644  aacllem  45255
  Copyright terms: Public domain W3C validator