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

Theorem 3impib 1144
Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
Hypothesis
Ref Expression
3impib.1 (𝜑 → ((𝜓𝜒) → 𝜃))
Assertion
Ref Expression
3impib ((𝜑𝜓𝜒) → 𝜃)

Proof of Theorem 3impib
StepHypRef Expression
1 3impib.1 . . 3 (𝜑 → ((𝜓𝜒) → 𝜃))
21expd 255 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
323imp 1140 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 927
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 929
This theorem is referenced by:  mob  2811  eqreu  2821  funimaexglem  5131  ssimaexg  5401  dfsmo2  6090  3ecoptocl  6421  distrnq0  7115  addassnq0  7118  uzind  8956  fzind  8960  fnn0ind  8961  xltnegi  9401  facwordi  10279  shftvalg  10401  shftval4g  10402  mulgcd  11448  coprmdvds1  11516  inopn  11870  basis1  11913  xmeteq0  12161  speano5  12563
  Copyright terms: Public domain W3C validator