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  5616  mpt2fun  5948  soxp  6230  oaass  6561  undifixp  6854  undom  6952  xpdom2  6959  tcrank  7556  inawinalem  8313  addcanpr  8672  ltsosr  8718  1re  8839  add42  9030  muladd  9214  mulsub  9224  divmuleq  9467  ltmul12a  9614  lemul12b  9615  lemul12a  9616  qaddcl  10334  qmulcl  10336  iooshf  10730  fzass4  10831  modid  10995  tanaddlem  12448  fpwipodrs  14269  issubg4  14640  ghmpreima  14706  cntzsubg  14814  islmodd  15635  lssvsubcl  15703  lssvscl  15714  lmhmf1o  15805  pwsdiaglmhm  15816  lidlsubcl  15970  fctop  16743  cctop  16745  opnneissb  16853  pnrmopn  17073  hausnei2  17083  txcnmpt  17320  txrest  17327  tx1stc  17346  fbssfi  17534  opnfbas  17539  rnelfmlem  17649  alexsubALTlem3  17745  metcnp3  18088  cncfmet  18414  evth  18459  caucfil  18711  ovolun  18860  dveflem  19328  efnnfsumcl  20342  efchtdvds  20399  lgsdir2  20569  hvsub4  21618  his35  21669  shscli  21898  5oalem2  22236  3oalem2  22244  hosub4  22395  hmops  22602  hmopm  22603  hmopco  22605  adjmul  22674  adjadd  22675  mdslmd1lem1  22907  mdslmd1lem2  22908  mulge0b  24088  dfon2lem6  24146  wfrlem4  24261  nofulllem4  24361  axdimuniq  24543  axcontlem2  24595  funline  24767  cbcpcp  25173  prdnei  25584  limptlimpr2lem2  25586  neibastop2lem  26320  fdc  26466  seqpo  26468  ismtyval  26535  mzpcompact2lem  26840  jm2.26  27106  paddss12  30081
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