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

Theorem imp42 597
Description: An importation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
imp4.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Assertion
Ref Expression
imp42  |-  ( ( ( ph  /\  ( ps  /\  ch ) )  /\  th )  ->  ta )

Proof of Theorem imp42
StepHypRef Expression
1 imp4.1 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
21imp32 434 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  -> 
( th  ->  ta ) )
32imp 430 1  |-  ( ( ( ph  /\  ( ps  /\  ch ) )  /\  th )  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  imp55  604  ltexprlem7  9466  iscatd  15530  isposd  16152  pospropd  16331  mulgghm2  18999  ordtbaslem  20135  txbas  20513  grporcan  25794  chirredlem1  27878  cvxpcon  29753  cvxscon  29754  nocvxminlem  30364  rngonegmn1l  31892  prnc  32004
  Copyright terms: Public domain W3C validator