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

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

Proof of Theorem 3impa
StepHypRef Expression
1 3impa.1 . . 3  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
21exp31 356 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
323imp 1133 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:  3impdir  1226  syl3an9b  1242  biimp3a  1277  stoic3  1361  rspec3  2456  rspc3v  2724  raltpg  3463  rextpg  3464  otexg  4013  opelopabt  4045  tpexg  4225  3optocl  4464  fun2ssres  4993  funssfv  5251  fvun1  5291  foco2  5370  f1elima  5464  eloprabga  5642  caovimo  5745  ot1stg  5830  ot2ndg  5831  ot3rdgg  5832  brtposg  5923  rdgexggg  6046  rdgivallem  6050  nnmass  6151  nndir  6154  nnaword  6171  th3q  6298  ecovass  6302  ecoviass  6303  findcard  6444  unfiin  6470  addasspig  6634  mulasspig  6636  mulcanpig  6639  ltapig  6642  ltmpig  6643  addassnqg  6686  ltbtwnnqq  6719  mulnnnq0  6754  addassnq0  6766  genpassl  6828  genpassu  6829  genpassg  6830  aptiprleml  6943  adddir  7224  le2tri3i  7338  addsub12  7440  subdir  7609  reapmul1  7814  recexaplem2  7861  div12ap  7901  divdiv32ap  7927  divdivap1  7930  lble  8144  zaddcllemneg  8523  fnn0ind  8596  xrltso  8999  iccgelb  9083  elicc4  9091  elfz  9163  fzrevral  9250  expivallem  9626  expnegap0  9633  expgt0  9658  expge0  9661  expge1  9662  mulexpzap  9665  expp1zap  9674  expm1ap  9675  abssubap0  10177  dvds0lem  10413  dvdsnegb  10420  muldvds1  10428  muldvds2  10429  divalgmodcl  10535  gcd2n0cl  10568  lcmdvds  10668  prmdvdsexp  10734  rpexp1i  10740
  Copyright terms: Public domain W3C validator