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

Theorem ad2ant2l 727
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 697 . 2  |-  ( (
ph  /\  ( ta  /\ 
ps ) )  ->  ch )
32adantll 695 1  |-  ( ( ( th  /\  ph )  /\  ( ta  /\  ps ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  mpteqb  5805  mpt2fun  6158  soxp  6445  oaass  6790  undifixp  7084  undom  7182  xpdom2  7189  tcrank  7792  inawinalem  8548  addcanpr  8907  ltsosr  8953  1re  9074  add42  9266  muladd  9450  mulsub  9460  divmuleq  9703  ltmul12a  9850  lemul12b  9851  lemul12a  9852  qaddcl  10574  qmulcl  10576  iooshf  10973  fzass4  11074  modid  11253  tanaddlem  12750  fpwipodrs  14573  issubg4  14944  ghmpreima  15010  cntzsubg  15118  islmodd  15939  lssvsubcl  16003  lssvscl  16014  lmhmf1o  16105  pwsdiaglmhm  16116  lidlsubcl  16270  fctop  17051  cctop  17053  opnneissb  17161  pnrmopn  17390  hausnei2  17400  neitx  17622  txcnmpt  17639  txrest  17646  tx1stc  17665  fbssfi  17852  opnfbas  17857  rnelfmlem  17967  alexsubALTlem3  18063  metcnp3  18553  cncfmet  18921  evth  18967  caucfil  19219  ovolun  19378  dveflem  19846  efnnfsumcl  20868  efchtdvds  20925  lgsdir2  21095  hvsub4  22522  his35  22573  shscli  22802  5oalem2  23140  3oalem2  23148  hosub4  23299  hmops  23506  hmopm  23507  hmopco  23509  adjmul  23578  adjadd  23579  mdslmd1lem1  23811  mdslmd1lem2  23812  mulge0b  25174  dfon2lem6  25394  wfrlem4  25509  nofulllem4  25609  axdimuniq  25795  axcontlem2  25847  funline  26019  mbfposadd  26195  itg2addnc  26200  neibastop2lem  26321  fdc  26381  seqpo  26383  ismtyval  26441  mzpcompact2lem  26740  jm2.26  27005  elfzomelpfzo  28031  paddss12  30347
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 178  df-an 361
  Copyright terms: Public domain W3C validator