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

Theorem 3ad2antl1 1117
Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)
Hypothesis
Ref Expression
3ad2antl.1  |-  ( (
ph  /\  ch )  ->  th )
Assertion
Ref Expression
3ad2antl1  |-  ( ( ( ph  /\  ps  /\ 
ta )  /\  ch )  ->  th )

Proof of Theorem 3ad2antl1
StepHypRef Expression
1 3ad2antl.1 . . 3  |-  ( (
ph  /\  ch )  ->  th )
21adantlr 695 . 2  |-  ( ( ( ph  /\  ta )  /\  ch )  ->  th )
323adantl2 1112 1  |-  ( ( ( ph  /\  ps  /\ 
ta )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  smorndom  6385  omeulem1  6580  dif1enOLD  7090  dif1en  7091  ordiso2  7230  infpssrlem4  7932  fin1a2lem9  8034  gchpwdom  8296  tskwun  8406  gruxp  8429  muldvds2  12554  dvds2add  12560  dvds2sub  12561  dvdstr  12562  mulgnnsubcl  14579  mulgpropd  14600  gexdvdsi  14894  rngidss  15367  reslmhm2  15810  issubassa  16064  obs2ss  16629  restntr  16912  cnpnei  16993  upxp  17317  qtopss  17406  opnfbas  17537  fbasrn  17579  trfg  17586  ufilmax  17602  prdsxmetlem  17932  nmoix  18238  nmoi2  18239  iimulcl  18435  mbfimaopn2  19012  lgsval4lem  20546  gxcl  20932  lnosub  21337  pjspansn  22156  cnpcon  23761  ghomf1olem  24001  nodenselem8  24342  brbtwn2  24533  colinearalg  24538  axsegconlem1  24545  11st22nd  25045  prjmapcp  25165  isppm  25354  rltrran  25414  istopxc  25548  lvsovso  25626  mettrifi  26473  ghomdiv  26574  grpokerinj  26575  rngohomco  26605  crngohomfo  26631  keridl  26657  mzpsubst  26826  lzunuz  26847  diophrex  26855  rmxycomplete  27002  jm2.26  27095  lnmepi  27183  lmhmlnmsplit  27185  lsslindf  27300  mndvcl  27446  mhmvlin  27452  fmul01lt1  27716  lub0N  29379  glb0N  29383  cvrcon3b  29467
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  df-3an 936
  Copyright terms: Public domain W3C validator