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

Theorem 3adantl3 1113
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 952 . 2  |-  ( (
ph  /\  ps  /\  ta )  ->  ( ph  /\  ps ) )
2 3adantl.1 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
31, 2sylan 457 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:  dif1enOLD  7177  dif1en  7178  infpssrlem4  8019  fin23lem11  8030  tskwun  8493  gruf  8520  lediv2a  9737  prunioo  10853  rpnnen2lem7  12590  muldvds1  12644  muldvds2  12645  dvdscmul  12646  dvdsmulc  12647  rpexp  12890  pospropd  14331  elcls  16910  cnpnei  17093  cnpflf2  17791  cnpflf  17792  cnpfcf  17832  xbln0  18061  blcls  18148  iimulcl  18533  icccvx  18546  iscau2  18801  cncombf  19111  mumul  20525  nvmul0or  21318  fh1  22305  fh2  22306  cm2j  22307  pjoi0  22404  hoadddi  22491  hmopco  22711  iscnp4  23447  volfiniune  23850  ax5seglem1  25115  ax5seglem2  25116  ivthALT  25582  rngohomco  25928  rngoisoco  25936  ibliccsinexp  27068  iblioosinexp  27070  pexmidlem3N  30213  hdmapglem7  32174
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