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

Theorem 3imp2 1195
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 1194 . 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 958
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 960
This theorem is referenced by:  wereu  4703  ovg  6218  fisup2g  7704  cfcoflem  8429  ttukeylem5  8670  dedekindle  9521  grplcan  15569  mulgnnass  15634  dmdprdsplit2  16518  mulgass2  16626  lmodvsdi  16894  lmodvsdir  16895  lmodvsass  16896  lss1d  16965  islmhm2  17040  lspsolvlem  17144  lbsextlem2  17161  cygznlem2a  17841  isphld  17924  t0dist  18770  hausnei  18773  nrmsep3  18800  fclsopni  19429  fcfneii  19451  ax5seglem5  23001  axcont  23044  grporcan  23530  grpolcan  23542  ghgrp  23677  slmdvsdi  26079  slmdvsdir  26080  slmdvsass  26081  broutsideof2  27999  frinfm  28470  crngm23  28643  pridl  28678  pridlc  28712  dmnnzd  28716  dmncan1  28717  paddasslem5  33038
  Copyright terms: Public domain W3C validator