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  5739  fvreseq0  5913  fliftfun  6115  omordi  7116  f1imaen2g  7481  isinf  7638  frfi  7669  acndom2  8336  infxp  8496  cff1  8539  isf32lem7  8640  fpwwe2lem12  8920  inawinalem  8968  inar1  9054  grur1  9099  genpnnp  9286  ltexprlem7  9323  prlem936  9328  reclem3pr  9330  1re  9497  addsub4  9764  muladd  9889  lt2add  9936  mullt0  9971  mulnzcnopr  10094  divmuldiv  10143  divmul24  10147  divmuleq  10148  recdiv  10149  divadddiv  10158  conjmul  10160  prodgt0  10286  ltmul12a  10297  lemul12b  10298  lediv12a  10337  lediv2a  10338  qmulcl  11083  irrmul  11090  xrrege0  11258  xmulge0  11359  ge0addcl  11515  ge0mulcl  11516  ge0xaddcl  11517  ge0xmulcl  11518  fzass4  11614  fzrev  11637  fzm1  11658  serge0  11978  expclzlem  12007  expge0  12018  expge1  12019  lt2sq  12057  le2sq  12058  bernneq  12108  wrdeqswrdlsw  12462  cshwleneq  12570  s2eq2seq  12663  sqrmo  12860  limsupval2  13077  o1lo12  13135  climrlim2  13144  2clim  13169  climsup  13266  tanaddlem  13569  divalglem8  13723  opeo  13999  omeo  14000  pcpremul  14029  pcmul  14037  setscom  14323  fpwipodrs  15454  grplactcnv  15744  resgrpisgrp  15822  ghmpreima  15888  ghmeql  15889  conjghm  15897  pgpfi  16226  lmodprop2d  17131  lidlmcl  17423  xrs1mnd  17977  absabv  17996  lmimco  18399  mavmulass  18488  mdetdiaglem  18537  cramerimplem2  18623  opnneissb  18851  cncnpi  19015  pnrmopn  19080  cmpsub  19136  connsub  19158  t1conperf  19173  neitx  19313  txcnmpt  19330  txrest  19337  txdis1cn  19341  tx1stc  19356  qtopcn  19420  trfg  19597  rnelfmlem  19658  flffbas  19701  nmo0  20447  nmoid  20454  cfilfcls  20918  iscmet3lem2  20936  caubl  20951  relcmpcmet  20960  ovolun  21115  ovolicc2lem3  21135  volsup  21171  ioombl1lem4  21176  ismbf3d  21266  mbfimaopnlem  21267  i1faddlem  21305  itgle  21421  ellimc2  21486  ftc1a  21643  dgrmul  21871  itgulm  22007  abelthlem8  22038  ptolemy  22092  logdivlt  22204  cxplt3  22279  cxple3  22280  o1cxp  22502  basellem4  22555  sqf11  22611  lgslem3  22771  lgsdir2  22801  lgsne0  22806  lgsquad3  22834  chpo1ubb  22864  vmadivsumb  22866  rpvmasumlem  22870  dchrisum0re  22896  dchrisum0  22903  selberg2b  22935  selberg3lem2  22941  pntrsumbnd  22949  pntrlog2bnd  22967  axcontlem2  23364  grporcan  23861  isgrp2d  23875  ablomul  23995  blocni  24358  ubthlem3  24426  htthlem  24472  hvsub4  24592  shscli  24873  elspansn4  25129  5oalem2  25211  hosub4  25370  hmops  25577  hmopco  25580  adjadd  25650  hstpyth  25786  hstles  25788  mdsl0  25867  mdslmd1lem2  25883  chirredlem1  25947  chirredlem2  25948  chirredlem3  25949  chirredlem4  25950  mdsymlem6  25965  cdj3lem2b  25994  resf1o  26182  esumpcvgval  26673  wfr3g  27868  frr3g  27912  nocvxmin  27977  heicant  28575  mblfinlem4  28580  ismblfin  28581  itg2addnc  28595  ftc1cnnc  28615  reftr  28710  tailfb  28747  filbcmb  28783  prdsbnd  28841  ismtyval  28848  heiborlem8  28866  ghomco  28897  mzpindd  29231  mulltgt0  29893  stoweidlem46  29990  2wlkeq  30437  usgra2adedgspth  30454  wwlkext2clwwlk  30614  zlmodzxzsubm  30905  zlmodzxzsub  30906
  Copyright terms: Public domain W3C validator