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

Theorem exp43 596
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
exp43.1  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  ->  ta )
Assertion
Ref Expression
exp43  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )

Proof of Theorem exp43
StepHypRef Expression
1 exp43.1 . . 3  |-  ( ( ( ph  /\  ps )  /\  ( ch  /\  th ) )  ->  ta )
21ex 424 . 2  |-  ( (
ph  /\  ps )  ->  ( ( ch  /\  th )  ->  ta )
)
32exp4b 591 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  exp53  601  funssres  5452  fvopab3ig  5762  fvmptt  5779  tfrlem2  6596  tfr3  6619  omordi  6768  odi  6781  nnmordi  6833  php  7250  fiint  7342  ordiso2  7440  cfcoflem  8108  zorn2lem5  8336  inar1  8606  psslinpr  8864  recexsrlem  8934  qaddcl  10546  qmulcl  10548  elfznelfzo  11147  expcan  11387  ltexp2  11388  bernneq  11460  expnbnd  11463  xpnnenOLD  12764  spwmo  14613  elcls3  17102  opnneissb  17133  txbas  17552  grpoidinvlem3  21747  grporcan  21762  shscli  22772  spansncol  23023  spanunsni  23034  spansncvi  23107  homco1  23257  homulass  23258  atomli  23838  chirredlem1  23846  cdj1i  23889  frinfm  26327  filbcmb  26332  unichnidl  26531  dmncan1  26576  pclfinclN  30432
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