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

Theorem 3impb 1099
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 1097 1 ((φ ψ χ) → θ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   w3a 884
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 886
This theorem is referenced by:  3adant1l  1126  3adant1r  1127  3impdi  1189  vtocl3gf  2610  rspc2ev  2658  reuss  3212  trssord  4083  funtp  4895  resdif  5091  funimass4  5167  fnovex  5481  fnotovb  5490  fovrn  5585  fnovrn  5590  fmpt2co  5779  nndi  6004  nnaordi  6017  ecovass  6151  ecoviass  6152  ecovdi  6153  ecovidi  6154  addasspig  6314  mulasspig  6316  distrpig  6317  distrnq0  6442  addassnq0  6445  distnq0r  6446  prcdnql  6467  prcunqu  6468  genpassl  6507  genpassu  6508  genpassg  6509  distrlem1prl  6558  distrlem1pru  6559  ltexprlemopl  6575  ltexprlemopu  6577  le2tri3i  6923  cnegexlem1  6983  subadd  7011  addsub  7019  subdi  7178  submul2  7192  div12ap  7455  diveqap1  7464  divnegap  7465  divdivap2  7482  ltmulgt11  7611  gt0div  7617  ge0div  7618  uzind3  8127  fnn0ind  8130  qdivcl  8352  irrmul  8356  xrlttr  8486  fzen  8677  iseqval  8900
  Copyright terms: Public domain W3C validator