ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  expd Unicode version

Theorem expd 254
Description: Exportation deduction. (Contributed by NM, 20-Aug-1993.)
Hypothesis
Ref Expression
exp3a.1  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Assertion
Ref Expression
expd  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )

Proof of Theorem expd
StepHypRef Expression
1 exp3a.1 . . . 4  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
21com12 30 . . 3  |-  ( ( ps  /\  ch )  ->  ( ph  ->  th )
)
32ex 113 . 2  |-  ( ps 
->  ( ch  ->  ( ph  ->  th ) ) )
43com3r 78 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106
This theorem is referenced by:  expdimp  255  pm3.3  257  syland  287  exp32  357  exp4c  360  exp4d  361  exp42  363  exp44  365  exp5c  368  impl  372  mpan2d  419  pm2.6dc  793  3impib  1137  exp5o  1158  biassdc  1327  exbir  1366  expcomd  1371  expdcom  1372  mopick  2020  ralrimivv  2443  mob2  2773  reuind  2796  difin  3208  reupick3  3256  suctr  4184  tfisi  4336  relop  4514  funcnvuni  4999  fnun  5036  mpteqb  5293  funfvima  5422  poxp  5884  nnmass  6131  supisoti  6482  axprecex  7108  ltnsym  7264  nn0lt2  8510  fzind  8543  fnn0ind  8544  btwnz  8547  lbzbi  8782  ledivge1le  8884  elfz0ubfz0  9213  elfzo0z  9270  fzofzim  9274  flqeqceilz  9400  leexp2r  9627  bernneq  9690  cau3lem  10138  climuni  10270  mulcn2  10289  dvdsabseq  10392  ndvdssub  10474  bezoutlemmain  10531  rplpwr  10560  algcvgblem  10575  euclemma  10669
  Copyright terms: Public domain W3C validator