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

Theorem 3imp2 1202
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 1201 . 2  |-  ( ph  ->  ( ( ps  /\  ch  /\  th )  ->  ta ) )
32imp 429 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967
This theorem is referenced by:  wereu  4721  ovg  6234  fisup2g  7721  cfcoflem  8446  ttukeylem5  8687  dedekindle  9539  grplcan  15595  mulgnnass  15660  dmdprdsplit2  16550  mulgass2  16697  lmodvsdi  16976  lmodvsdir  16977  lmodvsass  16978  lss1d  17049  islmhm2  17124  lspsolvlem  17228  lbsextlem2  17245  cygznlem2a  18005  isphld  18088  t0dist  18934  hausnei  18937  nrmsep3  18964  fclsopni  19593  fcfneii  19615  ax5seglem5  23184  axcont  23227  grporcan  23713  grpolcan  23725  ghgrp  23860  slmdvsdi  26236  slmdvsdir  26237  slmdvsass  26238  broutsideof2  28158  frinfm  28634  crngm23  28807  pridl  28842  pridlc  28876  dmnnzd  28880  dmncan1  28881  paddasslem5  33473
  Copyright terms: Public domain W3C validator