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

Theorem 3adantl3 1115
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)
Hypothesis
Ref Expression
3adantl.1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Assertion
Ref Expression
3adantl3  |-  ( ( ( ph  /\  ps  /\ 
ta )  /\  ch )  ->  th )

Proof of Theorem 3adantl3
StepHypRef Expression
1 3simpa 954 . 2  |-  ( (
ph  /\  ps  /\  ta )  ->  ( ph  /\  ps ) )
2 3adantl.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylan 458 1  |-  ( ( ( ph  /\  ps  /\ 
ta )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  dif1enOLD  7269  dif1en  7270  infpssrlem4  8112  fin23lem11  8123  tskwun  8585  gruf  8612  lediv2a  9829  prunioo  10950  rpnnen2lem7  12740  muldvds1  12794  muldvds2  12795  dvdscmul  12796  dvdsmulc  12797  rpexp  13040  pospropd  14481  elcls  17053  iscnp4  17242  cnpnei  17243  cnpflf2  17946  cnpflf  17947  cnpfcf  17987  xbln0  18332  blcls  18419  iimulcl  18826  icccvx  18839  iscau2  19094  cncombf  19410  mumul  20824  nvmul0or  21974  fh1  22961  fh2  22962  cm2j  22963  pjoi0  23060  hoadddi  23147  hmopco  23367  iocinif  23973  volfiniune  24373  ax5seglem1  25574  ax5seglem2  25575  ivthALT  26022  rngohomco  26274  rngoisoco  26282  ibliccsinexp  27406  iblioosinexp  27408  pexmidlem3N  30137  hdmapglem7  32098
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  df-3an 938
  Copyright terms: Public domain W3C validator