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

Theorem ad2ant2r 778
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)
Hypothesis
Ref Expression
ad2ant2.1 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
ad2ant2r (((𝜑𝜃) ∧ (𝜓𝜏)) → 𝜒)

Proof of Theorem ad2ant2r
StepHypRef Expression
1 ad2ant2.1 . . 3 ((𝜑𝜓) → 𝜒)
21adantrr 748 . 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:  disjxiun  4573  fundif  5835  funcnvqp  5852  foco  6023  fliftfun  6440  wfr3g  7278  omordi  7511  f1imaen2g  7881  isinf  8036  frfi  8068  acndom2  8738  infxp  8898  cff1  8941  isf32lem7  9042  fpwwe2lem12  9320  inawinalem  9368  inar1  9454  grur1  9499  genpnnp  9684  ltexprlem7  9721  prlem936  9726  reclem3pr  9728  1re  9896  addsub4  10176  muladd  10314  lt2add  10365  mullt0  10399  mulnzcnopr  10525  divmuldiv  10577  divmul24  10581  divmuleq  10582  recdiv  10583  divadddiv  10592  conjmul  10594  prodgt0  10720  ltmul12a  10731  lemul12b  10732  lediv12a  10768  lediv2a  10769  qmulcl  11641  irrmul  11648  xrrege0  11841  xmulge0  11946  ge0addcl  12114  ge0mulcl  12115  ge0xaddcl  12116  ge0xmulcl  12117  fzass4  12208  fzrev  12231  fzocatel  12357  serge0  12675  expclzlem  12704  expge0  12716  expge1  12717  lt2sq  12757  le2sq  12758  bernneq  12810  ccatw2s1p1  13214  ccatw2s1p2  13215  cshwleneq  13363  s2eq2seq  13481  sqrmo  13789  limsupval2  14008  o1lo12  14066  climrlim2  14075  2clim  14100  climsup  14197  tanaddlem  14684  opeo  14876  omeo  14877  divalglem8  14910  coprmproddvdslem  15163  pcpremul  15335  pcmul  15343  setscom  15680  fpwipodrs  16936  dfgrp3lem  17285  grplactcnv  17290  resgrpisgrp  17387  ghmpreima  17454  ghmeql  17455  conjghm  17463  pgpfi  17792  lmodprop2d  18697  lidlmcl  18987  xrs1mnd  19552  absabv  19571  frlmipval  19885  lmimco  19950  mavmulass  20122  mdetdiaglem  20171  cramerimplem2  20257  opnneissb  20676  cncnpi  20840  pnrmopn  20905  cmpsub  20961  connsub  20982  t1conperf  20997  neitx  21168  txcnmpt  21185  txrest  21192  txdis1cn  21196  tx1stc  21211  qtopcn  21275  trfg  21453  rnelfmlem  21514  flffbas  21557  nmo0  22297  nmoid  22304  cfilfcls  22825  iscmet3lem2  22843  caubl  22859  relcmpcmet  22868  ovolun  23019  ovolicc2lem3  23039  volsup  23076  ioombl1lem4  23081  ismbf3d  23172  mbfimaopnlem  23173  i1faddlem  23211  itgle  23327  ellimc2  23392  ftc1a  23549  dgrmul  23775  itgulm  23911  abelthlem8  23942  ptolemy  23997  logdivlt  24116  cxplt3  24191  cxple3  24192  o1cxp  24446  basellem4  24555  sqf11  24610  lgslem3  24769  lgsdir2  24800  lgsne0  24805  lgsquad3  24857  chpo1ubb  24915  vmadivsumb  24917  rpvmasumlem  24921  dchrisum0re  24947  dchrisum0  24954  selberg2b  24986  selberg3lem2  24992  pntrsumbnd  25000  pntrlog2bnd  25018  axcontlem2  25591  usgra2adedgspth  25935  2wlkeq  26029  wwlkext2clwwlk  26125  grporcan  26550  blocni  26878  ubthlem3  26946  htthlem  26992  hvsub4  27112  shscli  27394  elspansn4  27650  5oalem2  27732  hosub4  27890  hmops  28097  hmopco  28100  adjadd  28170  hstpyth  28306  hstles  28308  mdsl0  28387  mdslmd1lem2  28403  chirredlem1  28467  chirredlem2  28468  chirredlem3  28469  chirredlem4  28470  mdsymlem6  28485  cdj3lem2b  28514  1stpreimas  28700  mdetpmtr2  29052  esumpcvgval  29301  frr3g  30857  nocvxmin  30924  tailfb  31376  isbasisrelowllem1  32203  isbasisrelowllem2  32204  poimirlem14  32417  heicant  32438  mblfinlem4  32443  ismblfin  32444  itg2addnc  32458  ftc1cnnc  32478  filbcmb  32529  prdsbnd  32586  ismtyval  32593  heiborlem8  32611  ghomco  32684  mzpindd  36151  rp-fakenanass  36703  mulltgt0  38028  stoweidlem46  38763  fourierdlem73  38896  iccelpart  39796  bgoldbtbnd  40050  umgr2edg  40458  umgrvad2edg  40462  uhgrspan1  40549  1wlkeq  40860  wwlksext2clwwlk  41253  conngrv2edg  41384  frgrnbnb  41485  2zrngmmgm  41758  srhmsubc  41890  srhmsubcALTV  41909  zlmodzxzsubm  41952  zlmodzxzsub  41953
  Copyright terms: Public domain W3C validator