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  5477  fliftfun  5827  omordi  6580  f1imaen2g  6938  isinf  7092  frfi  7118  acndom2  7697  infxp  7857  cff1  7900  isf32lem7  8001  fpwwe2lem12  8279  inawinalem  8327  inar1  8413  grur1  8458  genpnnp  8645  ltexprlem7  8682  prlem936  8687  reclem3pr  8689  1re  8853  addsub4  9106  muladd  9228  lt2add  9275  mullt0  9309  mulnzcnopr  9430  divmuldiv  9476  divmul24  9480  divmuleq  9481  recdiv  9482  divadddiv  9491  conjmul  9493  prodgt0  9617  ltmul12a  9628  lemul12b  9629  lediv12a  9665  lediv2a  9666  qmulcl  10350  irrmul  10357  xrrege0  10519  xmulge0  10620  ge0addcl  10764  ge0mulcl  10765  ge0xaddcl  10766  ge0xmulcl  10767  fzass4  10845  fzrev  10862  fzm1  10878  serge0  11116  expclzlem  11143  expge0  11154  expge1  11155  lt2sq  11193  le2sq  11194  bernneq  11243  sqrmo  11753  limsupval2  11970  o1lo12  12028  climrlim2  12037  2clim  12062  climsup  12159  tanaddlem  12462  divalglem8  12615  opeo  12882  omeo  12883  pcpremul  12912  pcmul  12920  setscom  13192  fpwipodrs  14283  grplactcnv  14580  ghmpreima  14720  ghmeql  14721  conjghm  14729  pgpfi  14932  lmodprop2d  15703  lidlmcl  15985  xrs1mnd  16425  absabv  16445  opnneissb  16867  cncnpi  17023  pnrmopn  17087  cmpsub  17143  connsub  17163  t1conperf  17178  txcnmpt  17334  txrest  17341  txdis1cn  17345  tx1stc  17360  qtopcn  17421  trfg  17602  rnelfmlem  17663  flffbas  17706  nmo0  18260  nmoid  18267  cfilfcls  18716  iscmet3lem2  18734  caubl  18749  relcmpcmet  18758  ovolun  18874  ovolicc2lem3  18894  volsup  18929  ioombl1lem4  18934  ismbf3d  19025  mbfimaopnlem  19026  i1faddlem  19064  itgle  19180  ellimc2  19243  ftc1a  19400  dgrmul  19667  itgulm  19800  abelthlem8  19831  ptolemy  19880  logdivlt  19988  cxplt3  20063  cxple3  20064  o1cxp  20285  basellem4  20337  sqf11  20393  lgslem3  20553  lgsdir2  20583  lgsne0  20588  lgsquad3  20616  chpo1ubb  20646  vmadivsumb  20648  rpvmasumlem  20652  dchrisum0re  20678  dchrisum0  20685  selberg2b  20717  selberg3lem2  20723  pntrsumbnd  20731  pntrlog2bnd  20749  grporcan  20904  isgrp2d  20918  ablomul  21038  blocni  21399  ubthlem3  21467  htthlem  21513  hvsub4  21632  shscli  21912  elspansn4  22168  5oalem2  22250  hosub4  22409  hmops  22616  hmopco  22619  adjadd  22689  hstpyth  22825  hstles  22827  mdsl0  22906  mdslmd1lem2  22922  chirredlem1  22986  chirredlem2  22987  chirredlem3  22988  chirredlem4  22989  mdsymlem6  23004  cdj3lem2b  23033  esumpcvgval  23461  dmgmseqn0  23711  wfr3g  24326  frr3g  24351  nocvxmin  24416  axcontlem2  24665  ftc1cnnc  25025  prdnei  25676  limptlimpr2lem2  25678  eqidob  25898  clscnc  26113  reftr  26392  tailfb  26429  filbcmb  26535  prdsbnd  26620  ismtyval  26627  heiborlem8  26645  ghomco  26676  mzpindd  26927  mulltgt0  27796
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