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  3625  wefrc  4709  f1oweALT  6556  tfrlem9  6836  tz7.49  6892  oaordex  6989  dfac2  8292  zorn2lem4  8660  zorn2lem7  8663  psslinpr  9192  facwordi  12057  ndvdssub  13603  pmtrfrn  15955  elcls  18652  elcls3  18662  neibl  20051  met2ndc  20073  itgcn  21295  branmfn  25460  atcvatlem  25740  atcvat4i  25752  prtlem15  28973  cvlsupr4  32830  cvlsupr5  32831  cvlsupr6  32832  2llnneN  32893  cvrat4  32927  llnexchb2  33353  cdleme48gfv1  34020  cdlemg6e  34106  dihord6apre  34741  dihord5b  34744  dihord5apre  34747  dihglblem5apreN  34776  dihglbcpreN  34785
  Copyright terms: Public domain W3C validator