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  795  3impib  1139  exp5o  1160  biassdc  1329  exbir  1368  expcomd  1373  expdcom  1374  mopick  2023  ralrimivv  2450  mob2  2786  reuind  2809  difin  3225  reupick3  3273  suctr  4222  tfisi  4375  relop  4554  funcnvuni  5048  fnun  5085  mpteqb  5356  funfvima  5487  poxp  5954  nnmass  6202  supisoti  6649  axprecex  7359  ltnsym  7515  nn0lt2  8761  fzind  8794  fnn0ind  8795  btwnz  8798  lbzbi  9033  ledivge1le  9135  elfz0ubfz0  9464  elfzo0z  9523  fzofzim  9527  flqeqceilz  9653  leexp2r  9907  bernneq  9970  cau3lem  10442  climuni  10574  mulcn2  10593  dvdsabseq  10723  ndvdssub  10805  bezoutlemmain  10862  rplpwr  10891  algcvgblem  10906  euclemma  11000
  Copyright terms: Public domain W3C validator