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

Theorem 3impib 1179
 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 256 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
323imp 1175 1 ((𝜑𝜓𝜒) → 𝜃)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 962 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116  df-3an 964 This theorem is referenced by:  mob  2866  eqreu  2876  funimaexglem  5206  ssimaexg  5483  rbropap  6140  dfsmo2  6184  3ecoptocl  6518  distrnq0  7274  addassnq0  7277  uzind  9169  fzind  9173  fnn0ind  9174  xltnegi  9625  facwordi  10493  shftvalg  10615  shftval4g  10616  mulgcd  11710  coprmdvds1  11778  inopn  12179  basis1  12223  cnmpt2t  12471  cnmpt22  12472  cnmptcom  12476  xmeteq0  12537  sincosq1sgn  12923  sincosq2sgn  12924  sincosq3sgn  12925  sincosq4sgn  12926  speano5  13195
 Copyright terms: Public domain W3C validator