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  5721  mpt2fun  6072  soxp  6356  oaass  6701  undifixp  6995  undom  7093  xpdom2  7100  tcrank  7701  inawinalem  8458  addcanpr  8817  ltsosr  8863  1re  8984  add42  9175  muladd  9359  mulsub  9369  divmuleq  9612  ltmul12a  9759  lemul12b  9760  lemul12a  9761  qaddcl  10483  qmulcl  10485  iooshf  10881  fzass4  10982  modid  11157  tanaddlem  12654  fpwipodrs  14477  issubg4  14848  ghmpreima  14914  cntzsubg  15022  islmodd  15843  lssvsubcl  15911  lssvscl  15922  lmhmf1o  16013  pwsdiaglmhm  16024  lidlsubcl  16178  fctop  16958  cctop  16960  opnneissb  17068  pnrmopn  17288  hausnei2  17298  txcnmpt  17535  txrest  17542  tx1stc  17561  fbssfi  17745  opnfbas  17750  rnelfmlem  17860  alexsubALTlem3  17956  metcnp3  18299  cncfmet  18626  evth  18672  caucfil  18924  ovolun  19073  dveflem  19541  efnnfsumcl  20563  efchtdvds  20620  lgsdir2  20790  hvsub4  22050  his35  22101  shscli  22330  5oalem2  22668  3oalem2  22676  hosub4  22827  hmops  23034  hmopm  23035  hmopco  23037  adjmul  23106  adjadd  23107  mdslmd1lem1  23339  mdslmd1lem2  23340  mulge0b  24760  dfon2lem6  24970  wfrlem4  25085  nofulllem4  25185  axdimuniq  25368  axcontlem2  25420  funline  25592  neibastop2lem  25901  fdc  26047  seqpo  26049  ismtyval  26115  mzpcompact2lem  26420  jm2.26  26686  paddss12  30067
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