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

Theorem ad2ant2r 746
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 716 . 2  |-  ( (
ph  /\  ( ps  /\ 
ta ) )  ->  ch )
32adantlr 714 1  |-  ( ( ( ph  /\  th )  /\  ( ps  /\  ta ) )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  foco  5796  fvreseq0  5972  fliftfun  6189  omordi  7205  f1imaen2g  7566  isinf  7723  frfi  7754  acndom2  8424  infxp  8584  cff1  8627  isf32lem7  8728  fpwwe2lem12  9008  inawinalem  9056  inar1  9142  grur1  9187  genpnnp  9372  ltexprlem7  9409  prlem936  9414  reclem3pr  9416  1re  9584  addsub4  9851  muladd  9978  lt2add  10026  mullt0  10061  mulnzcnopr  10184  divmuldiv  10233  divmul24  10237  divmuleq  10238  recdiv  10239  divadddiv  10248  conjmul  10250  prodgt0  10376  ltmul12a  10387  lemul12b  10388  lediv12a  10427  lediv2a  10428  qmulcl  11189  irrmul  11196  xrrege0  11364  xmulge0  11465  ge0addcl  11621  ge0mulcl  11622  ge0xaddcl  11623  ge0xmulcl  11624  fzass4  11710  fzrev  11731  fzm1  11747  serge0  12117  expclzlem  12146  expge0  12157  expge1  12158  lt2sq  12196  le2sq  12197  bernneq  12247  wrdeqswrdlsw  12624  cshwleneq  12735  s2eq2seq  12832  sqrmo  13035  limsupval2  13252  o1lo12  13310  climrlim2  13319  2clim  13344  climsup  13441  tanaddlem  13751  divalglem8  13906  opeo  14185  omeo  14186  pcpremul  14215  pcmul  14223  setscom  14509  fpwipodrs  15640  grplactcnv  15932  resgrpisgrp  16010  ghmpreima  16076  ghmeql  16077  conjghm  16085  pgpfi  16414  lmodprop2d  17348  lidlmcl  17640  xrs1mnd  18217  absabv  18236  lmimco  18639  mavmulass  18811  mdetdiaglem  18860  cramerimplem2  18946  opnneissb  19374  cncnpi  19538  pnrmopn  19603  cmpsub  19659  connsub  19681  t1conperf  19696  neitx  19836  txcnmpt  19853  txrest  19860  txdis1cn  19864  tx1stc  19879  qtopcn  19943  trfg  20120  rnelfmlem  20181  flffbas  20224  nmo0  20970  nmoid  20977  cfilfcls  21441  iscmet3lem2  21459  caubl  21474  relcmpcmet  21483  ovolun  21638  ovolicc2lem3  21658  volsup  21694  ioombl1lem4  21699  ismbf3d  21789  mbfimaopnlem  21790  i1faddlem  21828  itgle  21944  ellimc2  22009  ftc1a  22166  dgrmul  22394  itgulm  22530  abelthlem8  22561  ptolemy  22615  logdivlt  22727  cxplt3  22802  cxple3  22803  o1cxp  23025  basellem4  23078  sqf11  23134  lgslem3  23294  lgsdir2  23324  lgsne0  23329  lgsquad3  23357  chpo1ubb  23387  vmadivsumb  23389  rpvmasumlem  23393  dchrisum0re  23419  dchrisum0  23426  selberg2b  23458  selberg3lem2  23464  pntrsumbnd  23472  pntrlog2bnd  23490  axcontlem2  23937  usgra2adedgspth  24275  2wlkeq  24369  wwlkext2clwwlk  24465  grporcan  24885  isgrp2d  24899  ablomul  25019  blocni  25382  ubthlem3  25450  htthlem  25496  hvsub4  25616  shscli  25897  elspansn4  26153  5oalem2  26235  hosub4  26394  hmops  26601  hmopco  26604  adjadd  26674  hstpyth  26810  hstles  26812  mdsl0  26891  mdslmd1lem2  26907  chirredlem1  26971  chirredlem2  26972  chirredlem3  26973  chirredlem4  26974  mdsymlem6  26989  cdj3lem2b  27018  resf1o  27211  esumpcvgval  27710  wfr3g  28905  frr3g  28949  nocvxmin  29014  heicant  29613  mblfinlem4  29618  ismblfin  29619  itg2addnc  29633  ftc1cnnc  29653  reftr  29748  tailfb  29785  filbcmb  29821  prdsbnd  29879  ismtyval  29886  heiborlem8  29904  ghomco  29935  mzpindd  30269  mulltgt0  30930  stoweidlem46  31301  fourierdlem73  31435  usgvad2edg  31813  zlmodzxzsubm  31887  zlmodzxzsub  31888
  Copyright terms: Public domain W3C validator