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

Theorem 3imp2 1211
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 1210 . 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 973
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 975
This theorem is referenced by:  wereu  4875  ovg  6423  fisup2g  7922  cfcoflem  8648  ttukeylem5  8889  dedekindle  9740  grplcan  15903  mulgnnass  15970  dmdprdsplit2  16885  mulgass2  17033  lmodvsdi  17318  lmodvsdir  17319  lmodvsass  17320  lss1d  17392  islmhm2  17467  lspsolvlem  17571  lbsextlem2  17588  cygznlem2a  18373  isphld  18456  t0dist  19592  hausnei  19595  nrmsep3  19622  fclsopni  20251  fcfneii  20273  ax5seglem5  23912  axcont  23955  grporcan  24899  grpolcan  24911  ghgrp  25046  slmdvsdi  27420  slmdvsdir  27421  slmdvsass  27422  broutsideof2  29349  frinfm  29829  crngm23  30002  pridl  30037  pridlc  30071  dmnnzd  30075  dmncan1  30076  paddasslem5  34620
  Copyright terms: Public domain W3C validator