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

Theorem 3expa 1115
Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)
Hypothesis
Ref Expression
3exp.1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
3expa  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )

Proof of Theorem 3expa
StepHypRef Expression
1 3exp.1 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213exp 1114 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp31 247 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    /\ w3a 896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  3anidm23  1205  mp3an2  1231  mpd3an3  1244  rgen3  2423  moi2  2744  sbc3ie  2858  preq12bg  3571  issod  4083  wepo  4123  reuhypd  4230  funimass4  5251  fvtp1g  5396  f1imass  5440  fcof1o  5456  f1ofveu  5527  f1ocnvfv3  5528  acexmid  5538  2ndrn  5836  rdgon  6003  frecrdg  6022  findcard  6375  findcard2  6376  findcard2s  6377  ltapig  6493  ltanqi  6557  ltmnqi  6558  lt2addnq  6559  lt2mulnq  6560  prarloclemcalc  6657  genpassl  6679  genpassu  6680  prmuloc  6721  ltexprlemm  6755  ltexprlemfl  6764  ltexprlemfu  6766  lteupri  6772  ltaprg  6774  mul4  7205  add4  7234  cnegexlem2  7249  cnegexlem3  7250  2addsub  7287  addsubeq4  7288  muladd  7452  ltleadd  7514  reapmul1  7659  apreim  7667  receuap  7723  p1le  7889  lemul12b  7901  zdiv  8385  fzind  8411  fnn0ind  8412  uzss  8588  qmulcl  8668  qreccl  8673  xrlttr  8816  icc0r  8895  iooshf  8921  elfz5  8983  elfz0fzfz0  9084  fzind2  9196  expnegap0  9422  expineg2  9423  mulexpzap  9454  expsubap  9462  expnbnd  9533  facndiv  9600  bccmpl  9615  ibcval5  9624  bcpasc  9627  crim  9679  climshftlemg  10046  dvdsval3  10104  dvdsnegb  10117  muldvds1  10124  muldvds2  10125  dvdscmul  10126  dvdsmulc  10127  dvds2ln  10132
  Copyright terms: Public domain W3C validator