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

Theorem 3imp2 1166
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 1165 . 2  |-  ( ph  ->  ( ( ps  /\  ch  /\  th )  ->  ta ) )
32imp 418 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  wereu  4389  ovg  5986  riotasv2dOLD  6350  riotasv3dOLD  6354  fisup2g  7217  cfcoflem  7898  ttukeylem5  8140  grplcan  14534  mulgnnass  14595  dmdprdsplit2  15281  mulgass2  15387  lmodvsdi  15650  lmodvsdir  15652  lmodvsass  15654  lss1d  15720  islmhm2  15795  lspsolvlem  15895  lbsextlem2  15912  cygznlem2a  16521  isphld  16558  t0dist  17053  hausnei  17056  nrmsep3  17083  fclsopni  17710  fcfneii  17732  grporcan  20888  grpolcan  20900  ghgrp  21035  dedekindle  24083  ax5seglem5  24561  axcont  24604  broutsideof2  24745  cmpmon  25815  icmpmon  25816  pdiveql  26168  frinfm  26416  crngm23  26627  pridl  26662  pridlc  26696  dmnnzd  26700  dmncan1  26701  paddasslem5  30013
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