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  4405  ovg  6002  riotasv2dOLD  6366  riotasv3dOLD  6370  fisup2g  7233  cfcoflem  7914  ttukeylem5  8156  grplcan  14550  mulgnnass  14611  dmdprdsplit2  15297  mulgass2  15403  lmodvsdi  15666  lmodvsdir  15668  lmodvsass  15670  lss1d  15736  islmhm2  15811  lspsolvlem  15911  lbsextlem2  15928  cygznlem2a  16537  isphld  16574  t0dist  17069  hausnei  17072  nrmsep3  17099  fclsopni  17726  fcfneii  17748  grporcan  20904  grpolcan  20916  ghgrp  21051  dedekindle  24098  ax5seglem5  24633  axcont  24676  broutsideof2  24817  cmpmon  25918  icmpmon  25919  pdiveql  26271  frinfm  26519  crngm23  26730  pridl  26765  pridlc  26799  dmnnzd  26803  dmncan1  26804  paddasslem5  30635
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