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

Theorem imp42 594
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 433 . 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
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
This theorem is referenced by:  imp55  601  ltexprlem7  9223  iscatd  14623  isposd  15137  pospropd  15316  mulgghm2  17937  mulgghm2OLD  17940  ordtbaslem  18804  txbas  19152  grporcan  23720  chirredlem1  25806  cvxpcon  27143  cvxscon  27144  nocvxminlem  27843  rngonegmn1l  28767  prnc  28879
  Copyright terms: Public domain W3C validator