MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3imp2 Structured version   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  4578  ovg  6212  riotasv2dOLD  6595  riotasv3dOLD  6599  fisup2g  7471  cfcoflem  8152  ttukeylem5  8393  grplcan  14857  mulgnnass  14918  dmdprdsplit2  15604  mulgass2  15710  lmodvsdi  15973  lmodvsdir  15974  lmodvsass  15975  lss1d  16039  islmhm2  16114  lspsolvlem  16214  lbsextlem2  16231  cygznlem2a  16848  isphld  16885  t0dist  17389  hausnei  17392  nrmsep3  17419  fclsopni  18047  fcfneii  18069  grporcan  21809  grpolcan  21821  ghgrp  21956  dedekindle  25188  ax5seglem5  25872  axcont  25915  broutsideof2  26056  frinfm  26437  crngm23  26612  pridl  26647  pridlc  26681  dmnnzd  26685  dmncan1  26686  paddasslem5  30621
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