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

Theorem ad2ant2r 798
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 753 . 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:  disjxiun  4681  fundif  5973  funcnvqp  5990  foco  6163  fliftfun  6602  wfr3g  7458  omordi  7691  f1imaen2g  8058  isinf  8214  frfi  8246  acndom2  8915  infxp  9075  cff1  9118  isf32lem7  9219  fpwwe2lem12  9501  inawinalem  9549  inar1  9635  grur1  9680  genpnnp  9865  ltexprlem7  9902  prlem936  9907  reclem3pr  9909  1re  10077  addsub4  10362  muladd  10500  lt2add  10551  mullt0  10585  mulnzcnopr  10711  divmuldiv  10763  divmul24  10767  divmuleq  10768  recdiv  10769  divadddiv  10778  conjmul  10780  prodgt0  10906  ltmul12a  10917  lemul12b  10918  lediv12a  10954  lediv2a  10955  qmulcl  11844  irrmul  11851  xrrege0  12043  xmulge0  12152  ge0addcl  12322  ge0mulcl  12323  ge0xaddcl  12324  ge0xmulcl  12325  fzass4  12417  fzrev  12441  fzocatel  12571  serge0  12895  expclzlem  12924  expge0  12936  expge1  12937  lt2sq  12977  le2sq  12978  bernneq  13030  ccatw2s1p1  13458  ccatw2s1p2  13459  cshwleneq  13609  s2eq2seq  13728  sqrmo  14036  limsupval2  14255  o1lo12  14313  climrlim2  14322  2clim  14347  climsup  14444  tanaddlem  14940  opeo  15136  omeo  15137  divalglem8  15170  coprmproddvdslem  15423  pcpremul  15595  pcmul  15603  setscom  15950  fpwipodrs  17211  dfgrp3lem  17560  grplactcnv  17565  resgrpisgrp  17662  ghmpreima  17729  ghmeql  17730  conjghm  17738  pgpfi  18066  lmodprop2d  18973  lidlmcl  19265  xrs1mnd  19832  absabv  19851  frlmipval  20166  lmimco  20231  mavmulass  20403  mdetdiaglem  20452  cramerimplem2  20538  opnneissb  20966  cncnpi  21130  pnrmopn  21195  cmpsub  21251  connsub  21272  t1connperf  21287  neitx  21458  txcnmpt  21475  txrest  21482  txdis1cn  21486  tx1stc  21501  qtopcn  21565  trfg  21742  rnelfmlem  21803  flffbas  21846  nmo0  22586  nmoid  22593  cfilfcls  23118  iscmet3lem2  23136  caubl  23152  relcmpcmet  23161  ovolun  23313  ovolicc2lem3  23333  volsup  23370  ioombl1lem4  23375  ismbf3d  23466  mbfimaopnlem  23467  i1faddlem  23505  itgle  23621  ellimc2  23686  ftc1a  23845  dgrmul  24071  itgulm  24207  abelthlem8  24238  ptolemy  24293  logdivlt  24412  cxplt3  24491  cxple3  24492  o1cxp  24746  basellem4  24855  sqf11  24910  lgslem3  25069  lgsdir2  25100  lgsne0  25105  lgsquad3  25157  chpo1ubb  25215  vmadivsumb  25217  rpvmasumlem  25221  dchrisum0re  25247  dchrisum0  25254  selberg2b  25286  selberg3lem2  25292  pntrsumbnd  25300  pntrlog2bnd  25318  axcontlem2  25890  umgr2edg  26146  umgrvad2edg  26150  uhgrspan1  26240  wlkeq  26585  wwlksext2clwwlk  27021  wwlksext2clwwlkOLD  27022  conngrv2edg  27173  frgrnbnb  27273  frgrwopreglem5lem  27300  frgrwopreglem5ALT  27302  grporcan  27500  blocni  27788  ubthlem3  27856  htthlem  27902  hvsub4  28022  shscli  28304  elspansn4  28560  5oalem2  28642  hosub4  28800  hmops  29007  hmopco  29010  adjadd  29080  hstpyth  29216  hstles  29218  mdsl0  29297  mdslmd1lem2  29313  chirredlem1  29377  chirredlem2  29378  chirredlem3  29379  chirredlem4  29380  mdsymlem6  29395  cdj3lem2b  29424  1stpreimas  29611  mdetpmtr2  30018  esumpcvgval  30268  frr3g  31904  nocvxmin  32019  tailfb  32497  isbasisrelowllem1  33333  isbasisrelowllem2  33334  poimirlem14  33553  heicant  33574  mblfinlem4  33579  ismblfin  33580  itg2addnc  33594  ftc1cnnc  33614  filbcmb  33665  prdsbnd  33722  ismtyval  33729  heiborlem8  33747  ghomco  33820  mzpindd  37626  rp-fakenanass  38177  mulltgt0  39495  stoweidlem46  40581  fourierdlem73  40714  iccelpart  41694  bgoldbtbnd  42022  2zrngmmgm  42271  srhmsubc  42401  srhmsubcALTV  42419  zlmodzxzsubm  42462  zlmodzxzsub  42463
  Copyright terms: Public domain W3C validator