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  8682  isposd  14105  pospropd  14254  mulgghm2  16475  ordtbaslem  16934  txbas  17278  grporcan  20904  chirredlem1  22986  cvxpcon  23788  cvxscon  23789  nocvxminlem  24415  rngonegmn1l  26683  prnc  26795
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