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

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

Proof of Theorem 3impa
StepHypRef Expression
1 3impa.1 . . 3 (((φ ψ) χ) → θ)
21exp31 346 . 2 (φ → (ψ → (χθ)))
323imp 1082 1 ((φ ψ χ) → θ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   w3a 871
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 873
This theorem is referenced by:  3impdir  1175  syl3an9b  1188  biimp3a  1218  rspec3  2383  rspc3v  2638  raltpg  3393  rextpg  3394  otexg  3937  opelopabt  3969  tpexg  4125  3optocl  4341  fun2ssres  4865  funssfv  5120  fvun1  5160  foco2  5239  f1elima  5333  eloprabga  5510  caovimo  5613  ot1stg  5698  ot2ndg  5699  ot3rdgg  5700  brtposg  5787  rdgexggg  5880  rdgivallem  5884  frecsuclem1  5899  nnmass  5977  nndir  5980  nnaword  5991  th3q  6118  ecovass  6122  ecoviass  6123  addasspig  6184  mulasspig  6186  mulcanpig  6189  ltapig  6192  ltmpig  6193  addassnqg  6235  ltbtwnnqq  6266  mulnnnq0  6299  addassnq0  6311  genpassl  6373  genpassu  6374  genpassg  6375  adddir  6614  addsub12  6811  subdir  6969
  Copyright terms: Public domain W3C validator