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