MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exp43 Structured version   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  5485  fvopab3ig  5795  fvmptt  5812  tfrlem2  6629  tfr3  6652  omordi  6801  odi  6814  nnmordi  6866  php  7283  fiint  7375  ordiso2  7476  cfcoflem  8144  zorn2lem5  8372  inar1  8642  psslinpr  8900  recexsrlem  8970  qaddcl  10582  qmulcl  10584  elfznelfzo  11184  expcan  11424  ltexp2  11425  bernneq  11497  expnbnd  11500  xpnnenOLD  12801  spwmo  14650  elcls3  17139  opnneissb  17170  txbas  17591  grpoidinvlem3  21786  grporcan  21801  shscli  22811  spansncol  23062  spanunsni  23073  spansncvi  23146  homco1  23296  homulass  23297  atomli  23877  chirredlem1  23885  cdj1i  23928  frinfm  26428  filbcmb  26433  unichnidl  26632  dmncan1  26677  pclfinclN  30684
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