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

Theorem 3impib 1113
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 249 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
323imp 1109 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  w3a 896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  mob  2745  eqreu  2755  funimaexglem  5009  ssimaexg  5262  dfsmo2  5932  3ecoptocl  6225  distrnq0  6614  addassnq0  6617  uzind  8407  fzind  8411  fnn0ind  8412  xltnegi  8848  facwordi  9601  shftvalg  9658  shftval4g  9659  speano5  10428
  Copyright terms: Public domain W3C validator