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

Theorem imp42 577
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 422 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  -> 
( th  ->  ta ) )
32imp 418 1  |-  ( ( ( ph  /\  ( ps  /\  ch ) )  /\  th )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  imp55  584  ltexprlem7  8666  isposd  14089  pospropd  14238  mulgghm2  16459  ordtbaslem  16918  txbas  17262  grporcan  20888  chirredlem1  22970  cvxpcon  23773  cvxscon  23774  nocvxminlem  24344  rngonegmn1l  26580  prnc  26692
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator