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  3760  wefrc  4859  f1oweALT  6765  tfrlem9  7052  tz7.49  7108  oaordex  7205  dfac2  8509  zorn2lem4  8877  zorn2lem7  8880  psslinpr  9407  facwordi  12341  ndvdssub  13937  pmtrfrn  16352  elcls  19440  elcls3  19450  neibl  20870  met2ndc  20892  itgcn  22115  branmfn  26889  atcvatlem  27169  atcvat4i  27181  prtlem15  30584  cvlsupr4  34772  cvlsupr5  34773  cvlsupr6  34774  2llnneN  34835  cvrat4  34869  llnexchb2  35295  cdleme48gfv1  35964  cdlemg6e  36050  dihord6apre  36685  dihord5b  36688  dihord5apre  36691  dihglblem5apreN  36720  dihglbcpreN  36729
  Copyright terms: Public domain W3C validator