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

Theorem ad2ant2r 728
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)
Hypothesis
Ref Expression
ad2ant2.1  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
ad2ant2r  |-  ( ( ( ph  /\  th )  /\  ( ps  /\  ta ) )  ->  ch )

Proof of Theorem ad2ant2r
StepHypRef Expression
1 ad2ant2.1 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
21adantrr 698 . 2  |-  ( (
ph  /\  ( ps  /\ 
ta ) )  ->  ch )
32adantlr 696 1  |-  ( ( ( ph  /\  th )  /\  ( ps  /\  ta ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  foco  5622  fliftfun  5993  omordi  6768  f1imaen2g  7127  isinf  7281  frfi  7311  acndom2  7891  infxp  8051  cff1  8094  isf32lem7  8195  fpwwe2lem12  8472  inawinalem  8520  inar1  8606  grur1  8651  genpnnp  8838  ltexprlem7  8875  prlem936  8880  reclem3pr  8882  1re  9046  addsub4  9300  muladd  9422  lt2add  9469  mullt0  9503  mulnzcnopr  9624  divmuldiv  9670  divmul24  9674  divmuleq  9675  recdiv  9676  divadddiv  9685  conjmul  9687  prodgt0  9811  ltmul12a  9822  lemul12b  9823  lediv12a  9859  lediv2a  9860  qmulcl  10548  irrmul  10555  xrrege0  10718  xmulge0  10819  ge0addcl  10965  ge0mulcl  10966  ge0xaddcl  10967  ge0xmulcl  10968  fzass4  11046  fzrev  11064  fzm1  11082  serge0  11332  expclzlem  11360  expge0  11371  expge1  11372  lt2sq  11410  le2sq  11411  bernneq  11460  sqrmo  12012  limsupval2  12229  o1lo12  12287  climrlim2  12296  2clim  12321  climsup  12418  tanaddlem  12722  divalglem8  12875  opeo  13142  omeo  13143  pcpremul  13172  pcmul  13180  setscom  13452  fpwipodrs  14545  grplactcnv  14842  ghmpreima  14982  ghmeql  14983  conjghm  14991  pgpfi  15194  lmodprop2d  15961  lidlmcl  16243  xrs1mnd  16691  absabv  16711  opnneissb  17133  cncnpi  17296  pnrmopn  17361  cmpsub  17417  connsub  17437  t1conperf  17452  neitx  17592  txcnmpt  17609  txrest  17616  txdis1cn  17620  tx1stc  17635  qtopcn  17699  trfg  17876  rnelfmlem  17937  flffbas  17980  nmo0  18722  nmoid  18729  cfilfcls  19180  iscmet3lem2  19198  caubl  19213  relcmpcmet  19222  ovolun  19348  ovolicc2lem3  19368  volsup  19403  ioombl1lem4  19408  ismbf3d  19499  mbfimaopnlem  19500  i1faddlem  19538  itgle  19654  ellimc2  19717  ftc1a  19874  dgrmul  20141  itgulm  20277  abelthlem8  20308  ptolemy  20357  logdivlt  20469  cxplt3  20544  cxple3  20545  o1cxp  20766  basellem4  20819  sqf11  20875  lgslem3  21035  lgsdir2  21065  lgsne0  21070  lgsquad3  21098  chpo1ubb  21128  vmadivsumb  21130  rpvmasumlem  21134  dchrisum0re  21160  dchrisum0  21167  selberg2b  21199  selberg3lem2  21205  pntrsumbnd  21213  pntrlog2bnd  21231  grporcan  21762  isgrp2d  21776  ablomul  21896  blocni  22259  ubthlem3  22327  htthlem  22373  hvsub4  22492  shscli  22772  elspansn4  23028  5oalem2  23110  hosub4  23269  hmops  23476  hmopco  23479  adjadd  23549  hstpyth  23685  hstles  23687  mdsl0  23766  mdslmd1lem2  23782  chirredlem1  23846  chirredlem2  23847  chirredlem3  23848  chirredlem4  23849  mdsymlem6  23864  cdj3lem2b  23893  esumpcvgval  24421  wfr3g  25469  frr3g  25494  nocvxmin  25559  axcontlem2  25808  mblfinlem3  26145  ismblfin  26146  itg2addnc  26158  ftc1cnnc  26178  reftr  26259  tailfb  26296  filbcmb  26332  prdsbnd  26392  ismtyval  26399  heiborlem8  26417  ghomco  26448  mzpindd  26693  mulltgt0  27560  stoweidlem46  27662  usgra2adedgspth  28045
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator