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

Theorem 3imp2 1214
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 1213 . 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 976
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 187  df-an 371  df-3an 978
This theorem is referenced by:  wereu  4821  ovg  6424  fisup2g  7962  cfcoflem  8686  ttukeylem5  8927  dedekindle  9781  grplcan  16428  mulgnnass  16496  dmdprdsplit2  17417  mulgass2  17569  lmodvsdi  17857  lmodvsdir  17858  lmodvsass  17859  lss1d  17931  islmhm2  18006  lspsolvlem  18110  lbsextlem2  18127  cygznlem2a  18906  isphld  18989  t0dist  20121  hausnei  20124  nrmsep3  20151  fclsopni  20810  fcfneii  20832  ax5seglem5  24665  axcont  24708  grporcan  25650  grpolcan  25662  ghgrpOLD  25797  slmdvsdi  28223  slmdvsdir  28224  slmdvsass  28225  mclsppslem  29808  broutsideof2  30473  frinfm  31521  crngm23  31694  pridl  31729  pridlc  31763  dmnnzd  31767  dmncan1  31768  paddasslem5  32854
  Copyright terms: Public domain W3C validator