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

Theorem 3impib 1139
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 254 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
323imp 1135 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  w3a 922
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 924
This theorem is referenced by:  mob  2787  eqreu  2797  funimaexglem  5053  ssimaexg  5314  dfsmo2  5987  3ecoptocl  6314  distrnq0  6939  addassnq0  6942  uzind  8767  fzind  8771  fnn0ind  8772  xltnegi  9206  facwordi  9997  shftvalg  10112  shftval4g  10113  mulgcd  10799  coprmdvds1  10867  speano5  11196
  Copyright terms: Public domain W3C validator