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  3731  wefrc  4815  f1oweALT  6664  tfrlem9  6947  tz7.49  7003  oaordex  7100  dfac2  8404  zorn2lem4  8772  zorn2lem7  8775  psslinpr  9304  facwordi  12175  ndvdssub  13722  pmtrfrn  16075  elcls  18802  elcls3  18812  neibl  20201  met2ndc  20223  itgcn  21446  branmfn  25654  atcvatlem  25934  atcvat4i  25946  prtlem15  29161  cvlsupr4  33299  cvlsupr5  33300  cvlsupr6  33301  2llnneN  33362  cvrat4  33396  llnexchb2  33822  cdleme48gfv1  34489  cdlemg6e  34575  dihord6apre  35210  dihord5b  35213  dihord5apre  35216  dihglblem5apreN  35245  dihglbcpreN  35254
  Copyright terms: Public domain W3C validator