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

Theorem expd 256
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 114 . 2  |-  ( ps 
->  ( ch  ->  ( ph  ->  th ) ) )
43com3r 79 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107
This theorem is referenced by:  expdimp  257  pm3.3  259  syland  291  exp32  362  exp4c  365  exp4d  366  exp42  368  exp44  370  exp5c  373  impl  377  mpan2d  424  a2and  547  pm2.6dc  847  3impib  1179  exp5o  1204  biassdc  1373  exbir  1412  expcomd  1417  expdcom  1418  mopick  2077  ralrimivv  2513  mob2  2864  reuind  2889  difin  3313  reupick3  3361  suctr  4343  tfisi  4501  relop  4689  funcnvuni  5192  fnun  5229  mpteqb  5511  funfvima  5649  poxp  6129  nnmass  6383  supisoti  6897  axprecex  7700  ltnsym  7862  nn0lt2  9144  fzind  9178  fnn0ind  9179  btwnz  9182  lbzbi  9420  ledivge1le  9525  elfz0ubfz0  9914  elfzo0z  9973  fzofzim  9977  flqeqceilz  10103  leexp2r  10359  bernneq  10424  cau3lem  10898  climuni  11074  mulcn2  11093  dvdsabseq  11556  ndvdssub  11638  bezoutlemmain  11697  rplpwr  11726  algcvgblem  11741  euclemma  11835  basis2  12229  txcnp  12454  metcnp3  12694
  Copyright terms: Public domain W3C validator