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

Theorem ad2ant2l 745
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)
Hypothesis
Ref Expression
ad2ant2.1  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
ad2ant2l  |-  ( ( ( th  /\  ph )  /\  ( ta  /\  ps ) )  ->  ch )

Proof of Theorem ad2ant2l
StepHypRef Expression
1 ad2ant2.1 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
21adantrl 715 . 2  |-  ( (
ph  /\  ( ta  /\ 
ps ) )  ->  ch )
32adantll 713 1  |-  ( ( ( th  /\  ph )  /\  ( ta  /\  ps ) )  ->  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:  mpteqb  5955  fvreseq0  5972  mpt2fun  6389  soxp  6898  oaass  7212  undifixp  7507  undom  7607  xpdom2  7614  tcrank  8305  inawinalem  9070  addcanpr  9427  ltsosr  9474  1re  9598  add42  9800  muladd  9996  mulsub  10006  divmuleq  10256  ltmul12a  10405  lemul12b  10406  lemul12a  10407  mulge0b  10419  qaddcl  11209  qmulcl  11211  iooshf  11614  fzass4  11732  elfzomelpfzo  11896  modid  12002  cshwleneq  12767  s2eq2seq  12864  tanaddlem  13883  fpwipodrs  15773  issubg4  16199  ghmpreima  16267  cntzsubg  16353  symgfixf1  16441  islmodd  17497  lssvsubcl  17569  lssvscl  17580  lmhmf1o  17671  pwsdiaglmhm  17682  lidlsubclOLD  17843  lmimco  18857  scmatghm  19013  scmatmhm  19014  mat2pmatscmxcl  19219  fctop  19483  cctop  19485  opnneissb  19593  pnrmopn  19822  hausnei2  19832  neitx  20086  txcnmpt  20103  txrest  20110  tx1stc  20129  fbssfi  20316  opnfbas  20321  rnelfmlem  20431  alexsubALTlem3  20527  metcnp3  21021  cncfmet  21390  evth  21437  caucfil  21700  ovolun  21888  dveflem  22358  efnnfsumcl  23354  efchtdvds  23411  lgsdir2  23581  axdimuniq  24194  axcontlem2  24246  friendship  25100  hvsub4  25932  his35  25983  shscli  26213  5oalem2  26551  3oalem2  26559  hosub4  26710  hmops  26917  hmopm  26918  hmopco  26920  adjmul  26989  adjadd  26990  mdslmd1lem1  27222  mdslmd1lem2  27223  elmrsubrn  28858  dfon2lem6  29196  wfrlem4  29322  nofulllem4  29441  funline  29768  mbfposadd  30038  itg2addnc  30045  neibastop2lem  30154  fdc  30214  seqpo  30216  ismtyval  30272  mzpcompact2lem  30660  jm2.26  30920  rnghmsubcsetclem2  32659  rhmsubcsetclem2  32702  rhmsubcrngclem2  32708  zlmodzxzsubm  32816  paddss12  35418
  Copyright terms: Public domain W3C validator