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

Theorem 3expa 1139
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 1138 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp31 252 1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    /\ w3a 920
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 922
This theorem is referenced by:  3anidm23  1229  mp3an2  1257  mpd3an3  1270  rgen3  2453  moi2  2782  sbc3ie  2896  preq12bg  3585  issod  4102  wepo  4142  reuhypd  4249  funimass4  5276  fvtp1g  5421  f1imass  5465  fcof1o  5480  f1ofveu  5551  f1ocnvfv3  5552  acexmid  5562  2ndrn  5860  frecrdg  6077  oawordriexmid  6134  findcard  6444  findcard2  6445  findcard2s  6446  ltapig  6642  ltanqi  6706  ltmnqi  6707  lt2addnq  6708  lt2mulnq  6709  prarloclemcalc  6806  genpassl  6828  genpassu  6829  prmuloc  6870  ltexprlemm  6904  ltexprlemfl  6913  ltexprlemfu  6915  lteupri  6921  ltaprg  6923  mul4  7359  add4  7388  cnegexlem2  7403  cnegexlem3  7404  2addsub  7441  addsubeq4  7442  muladd  7607  ltleadd  7669  reapmul1  7814  apreim  7822  receuap  7878  p1le  8046  lemul12b  8058  lbinf  8145  zdiv  8568  fzind  8595  fnn0ind  8596  uzss  8772  qmulcl  8855  qreccl  8860  xrlttr  8998  icc0r  9077  iooshf  9103  elfz5  9165  elfz0fzfz0  9266  fzind2  9377  ioo0  9398  ico0  9400  ioc0  9401  expnegap0  9633  expineg2  9634  mulexpzap  9665  expsubap  9673  expnbnd  9745  facndiv  9815  bccmpl  9830  ibcval5  9839  bcpasc  9842  crim  9946  climshftlemg  10342  dvdsval3  10407  dvdsnegb  10420  muldvds1  10428  muldvds2  10429  dvdscmul  10430  dvdsmulc  10431  dvds2ln  10436  divalgb  10532  ndvdssub  10537  gcddiv  10615  rpexp1i  10740  phiprmpw  10805  hashgcdeq  10811
  Copyright terms: Public domain W3C validator