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

Theorem 3impib 1203
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 258 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
323imp 1195 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  w3a 980
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117  df-3an 982
This theorem is referenced by:  mob  2934  eqreu  2944  iotam  5224  funimaexglem  5315  ssimaexg  5595  rbropap  6263  dfsmo2  6307  3ecoptocl  6645  distrnq0  7483  addassnq0  7486  uzind  9389  fzind  9393  fnn0ind  9394  xltnegi  9860  facwordi  10747  shftvalg  10872  shftval4g  10873  mulgcd  12044  coprmdvds1  12118  pcfac  12377  mgmcl  12828  mhmlin  12912  mhmmulg  13096  issubg2m  13121  nsgbi  13136  srgmulgass  13336  dvdsrtr  13444  issubrng2  13550  issubrg2  13581  inopn  13940  basis1  13984  cnmpt2t  14230  cnmpt22  14231  cnmptcom  14235  xmeteq0  14296  sincosq1sgn  14684  sincosq2sgn  14685  sincosq3sgn  14686  sincosq4sgn  14687  speano5  15134
  Copyright terms: Public domain W3C validator