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

Theorem exp43 595
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 423 . 2  |-  ( (
ph  /\  ps )  ->  ( ( ch  /\  th )  ->  ta )
)
32exp4b 590 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  exp53  600  funssres  5294  fvopab3ig  5599  fvmptt  5615  tfrlem2  6392  tfr3  6415  omordi  6564  odi  6577  nnmordi  6629  php  7045  fiint  7133  ordiso2  7230  cfcoflem  7898  zorn2lem5  8127  inar1  8397  psslinpr  8655  recexsrlem  8725  qaddcl  10332  qmulcl  10334  expcan  11154  ltexp2  11155  bernneq  11227  expnbnd  11230  xpnnenOLD  12488  spwmo  14335  elcls3  16820  opnneissb  16851  txbas  17262  grpoidinvlem3  20873  grporcan  20888  shscli  21896  spansncol  22147  spanunsni  22158  spansncvi  22231  homco1  22381  homulass  22382  atomli  22962  chirredlem1  22970  cdj1i  23013  cmpmon  25815  frinfm  26416  filbcmb  26432  unichnidl  26656  dmncan1  26701  pclfinclN  30139
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 177  df-an 360
  Copyright terms: Public domain W3C validator