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

Theorem imp42 578
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 423 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  -> 
( th  ->  ta ) )
32imp 419 1  |-  ( ( ( ph  /\  ( ps  /\  ch ) )  /\  th )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  imp55  585  ltexprlem7  8919  iscatd  13898  isposd  14412  pospropd  14561  mulgghm2  16786  ordtbaslem  17252  txbas  17599  grporcan  21809  chirredlem1  23893  cvxpcon  24929  cvxscon  24930  nocvxminlem  25645  rngonegmn1l  26565  prnc  26677
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 178  df-an 361
  Copyright terms: Public domain W3C validator