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

Theorem ad2ant2r 727
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 697 . 2  |-  ( (
ph  /\  ( ps  /\ 
ta ) )  ->  ch )
32adantlr 695 1  |-  ( ( ( ph  /\  th )  /\  ( ps  /\  ta ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  foco  5461  fliftfun  5811  omordi  6564  f1imaen2g  6922  isinf  7076  frfi  7102  acndom2  7681  infxp  7841  cff1  7884  isf32lem7  7985  fpwwe2lem12  8263  inawinalem  8311  inar1  8397  grur1  8442  genpnnp  8629  ltexprlem7  8666  prlem936  8671  reclem3pr  8673  1re  8837  addsub4  9090  muladd  9212  lt2add  9259  mullt0  9293  mulnzcnopr  9414  divmuldiv  9460  divmul24  9464  divmuleq  9465  recdiv  9466  divadddiv  9475  conjmul  9477  prodgt0  9601  ltmul12a  9612  lemul12b  9613  lediv12a  9649  lediv2a  9650  qmulcl  10334  irrmul  10341  xrrege0  10503  xmulge0  10604  ge0addcl  10748  ge0mulcl  10749  ge0xaddcl  10750  ge0xmulcl  10751  fzass4  10829  fzrev  10846  fzm1  10862  serge0  11100  expclzlem  11127  expge0  11138  expge1  11139  lt2sq  11177  le2sq  11178  bernneq  11227  sqrmo  11737  limsupval2  11954  o1lo12  12012  climrlim2  12021  2clim  12046  climsup  12143  tanaddlem  12446  divalglem8  12599  opeo  12866  omeo  12867  pcpremul  12896  pcmul  12904  setscom  13176  fpwipodrs  14267  grplactcnv  14564  ghmpreima  14704  ghmeql  14705  conjghm  14713  pgpfi  14916  lmodprop2d  15687  lidlmcl  15969  xrs1mnd  16409  absabv  16429  opnneissb  16851  cncnpi  17007  pnrmopn  17071  cmpsub  17127  connsub  17147  t1conperf  17162  txcnmpt  17318  txrest  17325  txdis1cn  17329  tx1stc  17344  qtopcn  17405  trfg  17586  rnelfmlem  17647  flffbas  17690  nmo0  18244  nmoid  18251  cfilfcls  18700  iscmet3lem2  18718  caubl  18733  relcmpcmet  18742  ovolun  18858  ovolicc2lem3  18878  volsup  18913  ioombl1lem4  18918  ismbf3d  19009  mbfimaopnlem  19010  i1faddlem  19048  itgle  19164  ellimc2  19227  ftc1a  19384  dgrmul  19651  itgulm  19784  abelthlem8  19815  ptolemy  19864  logdivlt  19972  cxplt3  20047  cxple3  20048  o1cxp  20269  basellem4  20321  sqf11  20377  lgslem3  20537  lgsdir2  20567  lgsne0  20572  lgsquad3  20600  chpo1ubb  20630  vmadivsumb  20632  rpvmasumlem  20636  dchrisum0re  20662  dchrisum0  20669  selberg2b  20701  selberg3lem2  20707  pntrsumbnd  20715  pntrlog2bnd  20733  grporcan  20888  isgrp2d  20902  ablomul  21022  blocni  21383  ubthlem3  21451  htthlem  21497  hvsub4  21616  shscli  21896  elspansn4  22152  5oalem2  22234  hosub4  22393  hmops  22600  hmopco  22603  adjadd  22673  hstpyth  22809  hstles  22811  mdsl0  22890  mdslmd1lem2  22906  chirredlem1  22970  chirredlem2  22971  chirredlem3  22972  chirredlem4  22973  mdsymlem6  22988  cdj3lem2b  23017  esumpcvgval  23446  dmgmseqn0  23696  wfr3g  24255  frr3g  24280  nocvxmin  24345  axcontlem2  24593  prdnei  25573  limptlimpr2lem2  25575  eqidob  25795  clscnc  26010  reftr  26289  tailfb  26326  filbcmb  26432  prdsbnd  26517  ismtyval  26524  heiborlem8  26542  ghomco  26573  mzpindd  26824  mulltgt0  27693
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 177  df-an 360
  Copyright terms: Public domain W3C validator