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

Theorem ad2ant2l 726
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 696 . 2  |-  ( (
ph  /\  ( ta  /\ 
ps ) )  ->  ch )
32adantll 694 1  |-  ( ( ( th  /\  ph )  /\  ( ta  /\  ps ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  mpteqb  5630  mpt2fun  5962  soxp  6244  oaass  6575  undifixp  6868  undom  6966  xpdom2  6973  tcrank  7570  inawinalem  8327  addcanpr  8686  ltsosr  8732  1re  8853  add42  9044  muladd  9228  mulsub  9238  divmuleq  9481  ltmul12a  9628  lemul12b  9629  lemul12a  9630  qaddcl  10348  qmulcl  10350  iooshf  10744  fzass4  10845  modid  11009  tanaddlem  12462  fpwipodrs  14283  issubg4  14654  ghmpreima  14720  cntzsubg  14828  islmodd  15649  lssvsubcl  15717  lssvscl  15728  lmhmf1o  15819  pwsdiaglmhm  15830  lidlsubcl  15984  fctop  16757  cctop  16759  opnneissb  16867  pnrmopn  17087  hausnei2  17097  txcnmpt  17334  txrest  17341  tx1stc  17360  fbssfi  17548  opnfbas  17553  rnelfmlem  17663  alexsubALTlem3  17759  metcnp3  18102  cncfmet  18428  evth  18473  caucfil  18725  ovolun  18874  dveflem  19342  efnnfsumcl  20356  efchtdvds  20413  lgsdir2  20583  hvsub4  21632  his35  21683  shscli  21912  5oalem2  22250  3oalem2  22258  hosub4  22409  hmops  22616  hmopm  22617  hmopco  22619  adjmul  22688  adjadd  22689  mdslmd1lem1  22921  mdslmd1lem2  22922  mulge0b  24101  dfon2lem6  24215  wfrlem4  24330  nofulllem4  24430  axdimuniq  24613  axcontlem2  24665  funline  24837  cbcpcp  25265  prdnei  25676  limptlimpr2lem2  25678  neibastop2lem  26412  fdc  26558  seqpo  26560  ismtyval  26627  mzpcompact2lem  26932  jm2.26  27198  paddss12  30630
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator