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

Theorem imp4a 573
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 434 . 2  |-  ( ( ( ch  /\  th )  ->  ta )  <->  ( ch  ->  ( th  ->  ta ) ) )
31, 2syl6ibr 219 1  |-  ( ph  ->  ( ps  ->  (
( ch  /\  th )  ->  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  imp4b  574  imp4d  576  imp55  585  imp511  586  reuss2  3613  wefrc  4568  f1oweALT  6066  riotasvdOLD  6585  tfrlem1  6628  tfrlem9  6638  tz7.49  6694  oaordex  6793  dfac2  8003  zorn2lem4  8371  zorn2lem7  8374  psslinpr  8900  facwordi  11572  ndvdssub  12919  elcls  17129  elcls3  17139  neibl  18523  met2ndc  18545  itgcn  19726  branmfn  23600  atcvatlem  23880  atcvat4i  23892  prtlem15  26705  pmtrfrn  27358  cvlsupr4  30070  cvlsupr5  30071  cvlsupr6  30072  2llnneN  30133  cvrat4  30167  llnexchb2  30593  cdleme48gfv1  31260  cdlemg6e  31346  dihord6apre  31981  dihord5b  31984  dihord5apre  31987  dihglblem5apreN  32016  dihglbcpreN  32025
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