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

Theorem 3imp2 1168
Description: Importation to right triple conjunction. (Contributed by NM, 26-Oct-2006.)
Hypothesis
Ref Expression
3imp1.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Assertion
Ref Expression
3imp2  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ta )

Proof of Theorem 3imp2
StepHypRef Expression
1 3imp1.1 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
213impd 1167 . 2  |-  ( ph  ->  ( ( ps  /\  ch  /\  th )  ->  ta ) )
32imp 419 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  wereu  4538  ovg  6171  riotasv2dOLD  6554  riotasv3dOLD  6558  fisup2g  7427  cfcoflem  8108  ttukeylem5  8349  grplcan  14812  mulgnnass  14873  dmdprdsplit2  15559  mulgass2  15665  lmodvsdi  15928  lmodvsdir  15929  lmodvsass  15930  lss1d  15994  islmhm2  16069  lspsolvlem  16169  lbsextlem2  16186  cygznlem2a  16803  isphld  16840  t0dist  17343  hausnei  17346  nrmsep3  17373  fclsopni  18000  fcfneii  18022  grporcan  21762  grpolcan  21774  ghgrp  21909  dedekindle  25141  ax5seglem5  25776  axcont  25819  broutsideof2  25960  frinfm  26327  crngm23  26502  pridl  26537  pridlc  26571  dmnnzd  26575  dmncan1  26576  paddasslem5  30306
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