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

Theorem 3impib 1102
 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 245 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
323imp 1098 1 ((𝜑𝜓𝜒) → 𝜃)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ∧ w3a 885 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 887 This theorem is referenced by:  mob  2723  eqreu  2733  funimaexglem  4982  ssimaexg  5235  dfsmo2  5902  3ecoptocl  6195  distrnq0  6557  addassnq0  6560  uzind  8349  fzind  8353  fnn0ind  8354  xltnegi  8748  shftvalg  9437  shftval4g  9438  speano5  10069
 Copyright terms: Public domain W3C validator