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  5625  fvreseq0  5798  fliftfun  6000  omordi  6997  f1imaen2g  7362  isinf  7518  frfi  7549  acndom2  8216  infxp  8376  cff1  8419  isf32lem7  8520  fpwwe2lem12  8800  inawinalem  8848  inar1  8934  grur1  8979  genpnnp  9166  ltexprlem7  9203  prlem936  9208  reclem3pr  9210  1re  9377  addsub4  9644  muladd  9769  lt2add  9816  mullt0  9851  mulnzcnopr  9974  divmuldiv  10023  divmul24  10027  divmuleq  10028  recdiv  10029  divadddiv  10038  conjmul  10040  prodgt0  10166  ltmul12a  10177  lemul12b  10178  lediv12a  10217  lediv2a  10218  qmulcl  10963  irrmul  10970  xrrege0  11138  xmulge0  11239  ge0addcl  11389  ge0mulcl  11390  ge0xaddcl  11391  ge0xmulcl  11392  fzass4  11488  fzrev  11511  fzm1  11532  serge0  11852  expclzlem  11881  expge0  11892  expge1  11893  lt2sq  11931  le2sq  11932  bernneq  11982  wrdeqswrdlsw  12335  cshwleneq  12443  s2eq2seq  12536  sqrmo  12733  limsupval2  12950  o1lo12  13008  climrlim2  13017  2clim  13042  climsup  13139  tanaddlem  13442  divalglem8  13596  opeo  13872  omeo  13873  pcpremul  13902  pcmul  13910  setscom  14196  fpwipodrs  15326  grplactcnv  15615  resgrpisgrp  15693  ghmpreima  15759  ghmeql  15760  conjghm  15768  pgpfi  16095  lmodprop2d  16985  lidlmcl  17276  xrs1mnd  17826  absabv  17845  lmimco  18248  mavmulass  18335  cramerimplem2  18465  opnneissb  18693  cncnpi  18857  pnrmopn  18922  cmpsub  18978  connsub  19000  t1conperf  19015  neitx  19155  txcnmpt  19172  txrest  19179  txdis1cn  19183  tx1stc  19198  qtopcn  19262  trfg  19439  rnelfmlem  19500  flffbas  19543  nmo0  20289  nmoid  20296  cfilfcls  20760  iscmet3lem2  20778  caubl  20793  relcmpcmet  20802  ovolun  20957  ovolicc2lem3  20977  volsup  21012  ioombl1lem4  21017  ismbf3d  21107  mbfimaopnlem  21108  i1faddlem  21146  itgle  21262  ellimc2  21327  ftc1a  21484  dgrmul  21712  itgulm  21848  abelthlem8  21879  ptolemy  21933  logdivlt  22045  cxplt3  22120  cxple3  22121  o1cxp  22343  basellem4  22396  sqf11  22452  lgslem3  22612  lgsdir2  22642  lgsne0  22647  lgsquad3  22675  chpo1ubb  22705  vmadivsumb  22707  rpvmasumlem  22711  dchrisum0re  22737  dchrisum0  22744  selberg2b  22776  selberg3lem2  22782  pntrsumbnd  22790  pntrlog2bnd  22808  axcontlem2  23162  grporcan  23659  isgrp2d  23673  ablomul  23793  blocni  24156  ubthlem3  24224  htthlem  24270  hvsub4  24390  shscli  24671  elspansn4  24927  5oalem2  25009  hosub4  25168  hmops  25375  hmopco  25378  adjadd  25448  hstpyth  25584  hstles  25586  mdsl0  25665  mdslmd1lem2  25681  chirredlem1  25745  chirredlem2  25746  chirredlem3  25747  chirredlem4  25748  mdsymlem6  25763  cdj3lem2b  25792  resf1o  25981  esumpcvgval  26479  wfr3g  27674  frr3g  27718  nocvxmin  27783  heicant  28379  mblfinlem4  28384  ismblfin  28385  itg2addnc  28399  ftc1cnnc  28419  reftr  28514  tailfb  28551  filbcmb  28587  prdsbnd  28645  ismtyval  28652  heiborlem8  28670  ghomco  28701  mzpindd  29035  mulltgt0  29697  stoweidlem46  29794  2wlkeq  30241  usgra2adedgspth  30258  wwlkext2clwwlk  30418  zlmodzxzsubm  30707  zlmodzxzsub  30708  mdetdiaglem  30824
  Copyright terms: Public domain W3C validator