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

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

Proof of Theorem imp4a
StepHypRef Expression
1 imp4.1 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
2 impexp 446 . 2  |-  ( ( ( ch  /\  th )  ->  ta )  <->  ( ch  ->  ( th  ->  ta ) ) )
31, 2syl6ibr 227 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:  imp4b  590  imp4d  592  imp55  601  imp511  602  reuss2  3771  wefrc  4866  f1oweALT  6758  tfrlem9  7044  tz7.49  7100  oaordex  7197  dfac2  8500  zorn2lem4  8868  zorn2lem7  8871  psslinpr  9398  facwordi  12322  ndvdssub  13913  pmtrfrn  16272  elcls  19333  elcls3  19343  neibl  20732  met2ndc  20754  itgcn  21977  branmfn  26550  atcvatlem  26830  atcvat4i  26842  prtlem15  30071  cvlsupr4  34017  cvlsupr5  34018  cvlsupr6  34019  2llnneN  34080  cvrat4  34114  llnexchb2  34540  cdleme48gfv1  35207  cdlemg6e  35293  dihord6apre  35928  dihord5b  35931  dihord5apre  35934  dihglblem5apreN  35963  dihglbcpreN  35972
  Copyright terms: Public domain W3C validator