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

Theorem ad2ant2r 744
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 714 . 2  |-  ( (
ph  /\  ( ps  /\ 
ta ) )  ->  ch )
32adantlr 712 1  |-  ( ( ( ph  /\  th )  /\  ( ps  /\  ta ) )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  foco  5787  fvreseq0  5963  fliftfun  6185  omordi  7207  f1imaen2g  7569  isinf  7726  frfi  7757  acndom2  8426  infxp  8586  cff1  8629  isf32lem7  8730  fpwwe2lem12  9008  inawinalem  9056  inar1  9142  grur1  9187  genpnnp  9372  ltexprlem7  9409  prlem936  9414  reclem3pr  9416  1re  9584  addsub4  9853  muladd  9985  lt2add  10033  mullt0  10068  mulnzcnopr  10191  divmuldiv  10240  divmul24  10244  divmuleq  10245  recdiv  10246  divadddiv  10255  conjmul  10257  prodgt0  10383  ltmul12a  10394  lemul12b  10395  lediv12a  10433  lediv2a  10434  qmulcl  11201  irrmul  11208  xrrege0  11378  xmulge0  11479  ge0addcl  11635  ge0mulcl  11636  ge0xaddcl  11637  ge0xmulcl  11638  fzass4  11725  fzrev  11746  fzocatel  11861  serge0  12146  expclzlem  12175  expge0  12187  expge1  12188  lt2sq  12226  le2sq  12227  bernneq  12277  ccatw2s1p1  12632  ccatw2s1p2  12633  cshwleneq  12779  s2eq2seq  12876  sqrmo  13170  limsupval2  13388  o1lo12  13446  climrlim2  13455  2clim  13480  climsup  13577  tanaddlem  13986  divalglem8  14145  opeo  14424  omeo  14425  pcpremul  14454  pcmul  14462  setscom  14751  fpwipodrs  15996  grplactcnv  16340  resgrpisgrp  16424  ghmpreima  16490  ghmeql  16491  conjghm  16499  pgpfi  16827  lmodprop2d  17770  lidlmcl  18063  xrs1mnd  18654  absabv  18673  frlmipval  18984  lmimco  19049  mavmulass  19221  mdetdiaglem  19270  cramerimplem2  19356  opnneissb  19785  cncnpi  19949  pnrmopn  20014  cmpsub  20070  connsub  20091  t1conperf  20106  neitx  20277  txcnmpt  20294  txrest  20301  txdis1cn  20305  tx1stc  20320  qtopcn  20384  trfg  20561  rnelfmlem  20622  flffbas  20665  nmo0  21411  nmoid  21418  cfilfcls  21882  iscmet3lem2  21900  caubl  21915  relcmpcmet  21924  ovolun  22079  ovolicc2lem3  22099  volsup  22135  ioombl1lem4  22140  ismbf3d  22230  mbfimaopnlem  22231  i1faddlem  22269  itgle  22385  ellimc2  22450  ftc1a  22607  dgrmul  22836  itgulm  22972  abelthlem8  23003  ptolemy  23058  logdivlt  23177  cxplt3  23252  cxple3  23253  o1cxp  23505  basellem4  23558  sqf11  23614  lgslem3  23774  lgsdir2  23804  lgsne0  23809  lgsquad3  23837  chpo1ubb  23867  vmadivsumb  23869  rpvmasumlem  23873  dchrisum0re  23899  dchrisum0  23906  selberg2b  23938  selberg3lem2  23944  pntrsumbnd  23952  pntrlog2bnd  23970  axcontlem2  24473  usgra2adedgspth  24818  2wlkeq  24912  wwlkext2clwwlk  25008  grporcan  25424  isgrp2d  25438  ablomul  25558  blocni  25921  ubthlem3  25989  htthlem  26035  hvsub4  26155  shscli  26436  elspansn4  26692  5oalem2  26774  hosub4  26933  hmops  27140  hmopco  27143  adjadd  27213  hstpyth  27349  hstles  27351  mdsl0  27430  mdslmd1lem2  27446  chirredlem1  27510  chirredlem2  27511  chirredlem3  27512  chirredlem4  27513  mdsymlem6  27528  cdj3lem2b  27557  1stpreimas  27755  esumpcvgval  28310  wfr3g  29585  frr3g  29629  nocvxmin  29694  heicant  30292  mblfinlem4  30297  ismblfin  30298  itg2addnc  30312  ftc1cnnc  30332  tailfb  30438  filbcmb  30474  prdsbnd  30532  ismtyval  30539  heiborlem8  30557  ghomco  30588  mzpindd  30921  mulltgt0  31640  stoweidlem46  32070  fourierdlem73  32204  usgvad2edg  32802  2zrngmmgm  33025  srhmsubc  33157  srhmsubcALTV  33176  zlmodzxzsubm  33221  zlmodzxzsub  33222  rp-fakenanass  38172
  Copyright terms: Public domain W3C validator