ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3impb Structured version   GIF version

Theorem 3impb 1081
Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)
Hypothesis
Ref Expression
3impb.1 ((φ (ψ χ)) → θ)
Assertion
Ref Expression
3impb ((φ ψ χ) → θ)

Proof of Theorem 3impb
StepHypRef Expression
1 3impb.1 . . 3 ((φ (ψ χ)) → θ)
21exp32 347 . 2 (φ → (ψ → (χθ)))
323imp 1079 1 ((φ ψ χ) → θ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   w3a 867
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110  df-3an 869
This theorem is referenced by:  3adant1l  1108  3adant1r  1109  3impdi  1171  vtocl3gf  2585  rspc2ev  2633  reuss  3187  trssord  4056  funtp  4867  resdif  5062  funimass4  5138  fnovex  5451  fnotovb  5460  fovrn  5555  fnovrn  5560  fmpt2co  5749  nndi  5969  nnaordi  5981  ecovass  6115  ecoviass  6116  ecovdi  6117  ecovidi  6118  addasspig  6177  mulasspig  6179  distrpig  6180  distrnq0  6301  addassnq0  6304  distnq0r  6305  prcdnql  6325  prcunqu  6326  genpassl  6366  genpassu  6367  genpassg  6368  distrlem1prl  6408  distrlem1pru  6409  ltexprlemopl  6425  ltexprlemopu  6427  le2tri3i  6727  cnegexlem1  6787  subadd  6815  addsub  6823  subdi  6982  submul2  6996  div12ap  7259  diveqap1  7268  divnegap  7269  divdivap2  7286  ltmulgt11  7414  gt0div  7420  ge0div  7421  uzind3  7917  fnn0ind  7920  qdivcl  8060  irrmul  8064  xrlttr  8193
  Copyright terms: Public domain W3C validator