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

Theorem imp4a 572
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 433 . 2  |-  ( ( ( ch  /\  th )  ->  ta )  <->  ( ch  ->  ( th  ->  ta ) ) )
31, 2syl6ibr 218 1  |-  ( ph  ->  ( ps  ->  (
( ch  /\  th )  ->  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  imp4b  573  imp4d  575  imp55  584  imp511  585  reuss2  3448  wefrc  4387  f1oweALT  5851  riotasvdOLD  6348  tfrlem1  6391  tfrlem9  6401  tz7.49  6457  oaordex  6556  dfac2  7757  zorn2lem4  8126  zorn2lem7  8129  psslinpr  8655  facwordi  11302  ndvdssub  12606  elcls  16810  elcls3  16820  neibl  18047  met2ndc  18069  itgcn  19197  branmfn  22685  atcvatlem  22965  atcvat4i  22977  and4as  24939  prtlem15  26743  pmtrfrn  27400  cvlsupr4  29535  cvlsupr5  29536  cvlsupr6  29537  2llnneN  29598  cvrat4  29632  llnexchb2  30058  cdleme48gfv1  30725  cdlemg6e  30811  dihord6apre  31446  dihord5b  31449  dihord5apre  31452  dihglblem5apreN  31481  dihglbcpreN  31490
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