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

Theorem 3imp2 1169
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 1168 . 2  |-  ( ph  ->  ( ( ps  /\  ch  /\  th )  ->  ta ) )
32imp 420 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  wereu  4580  ovg  6214  riotasv2dOLD  6597  riotasv3dOLD  6601  fisup2g  7473  cfcoflem  8154  ttukeylem5  8395  grplcan  14859  mulgnnass  14920  dmdprdsplit2  15606  mulgass2  15712  lmodvsdi  15975  lmodvsdir  15976  lmodvsass  15977  lss1d  16041  islmhm2  16116  lspsolvlem  16216  lbsextlem2  16233  cygznlem2a  16850  isphld  16887  t0dist  17391  hausnei  17394  nrmsep3  17421  fclsopni  18049  fcfneii  18071  grporcan  21811  grpolcan  21823  ghgrp  21958  dedekindle  25190  ax5seglem5  25874  axcont  25917  broutsideof2  26058  frinfm  26439  crngm23  26614  pridl  26649  pridlc  26683  dmnnzd  26687  dmncan1  26688  paddasslem5  30683
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator