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

Theorem ad2ant2l 750
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 720 . 2  |-  ( (
ph  /\  ( ta  /\ 
ps ) )  ->  ch )
32adantll 718 1  |-  ( ( ( th  /\  ph )  /\  ( ta  /\  ps ) )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  mpteqb  5977  fvreseq0  5994  mpt2fun  6409  soxp  6917  wfrlem4  7044  oaass  7267  undifixp  7563  undom  7663  xpdom2  7670  tcrank  8357  inawinalem  9115  addcanpr  9472  ltsosr  9519  1re  9643  add42  9851  muladd  10052  mulsub  10062  divmuleq  10313  ltmul12a  10462  lemul12b  10463  lemul12a  10464  mulge0b  10476  qaddcl  11281  qmulcl  11283  iooshf  11714  fzass4  11837  elfzomelpfzo  12013  modid  12121  cshwleneq  12907  s2eq2seq  13008  tanaddlem  14208  fpwipodrs  16398  issubg4  16824  ghmpreima  16892  cntzsubg  16978  symgfixf1  17066  islmodd  18085  lssvsubcl  18155  lssvscl  18166  lmhmf1o  18257  pwsdiaglmhm  18268  lidlsubclOLD  18428  lmimco  19389  scmatghm  19545  scmatmhm  19546  mat2pmatscmxcl  19751  fctop  20006  cctop  20008  opnneissb  20117  pnrmopn  20346  hausnei2  20356  neitx  20609  txcnmpt  20626  txrest  20633  tx1stc  20652  fbssfi  20839  opnfbas  20844  rnelfmlem  20954  alexsubALTlem3  21051  metcnp3  21542  cncfmet  21927  evth  21974  caucfil  22240  ovolun  22439  dveflem  22918  efnnfsumcl  24016  efchtdvds  24073  lgsdir2  24243  axdimuniq  24930  axcontlem2  24982  friendship  25836  hvsub4  26676  his35  26727  shscli  26956  5oalem2  27294  3oalem2  27302  hosub4  27452  hmops  27659  hmopm  27660  hmopco  27662  adjmul  27731  adjadd  27732  mdslmd1lem1  27964  mdslmd1lem2  27965  elmrsubrn  30154  dfon2lem6  30429  nofulllem4  30587  funline  30902  neibastop2lem  31009  isbasisrelowllem1  31699  isbasisrelowllem2  31700  mbfposadd  31902  itg2addnc  31910  fdc  31988  seqpo  31990  ismtyval  32046  paddss12  33303  mzpcompact2lem  35512  jm2.26  35777  rnghmsubcsetclem2  39250  rhmsubcsetclem2  39296  rhmsubcrngclem2  39302  zlmodzxzsubm  39414  ltsubaddb  39585  ltsubsubb  39586
  Copyright terms: Public domain W3C validator