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

Theorem 3expib 1118
Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)
Hypothesis
Ref Expression
3exp.1 ((𝜑𝜓𝜒) → 𝜃)
Assertion
Ref Expression
3expib (𝜑 → ((𝜓𝜒) → 𝜃))

Proof of Theorem 3expib
StepHypRef Expression
1 3exp.1 . . 3 ((𝜑𝜓𝜒) → 𝜃)
213exp 1114 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32impd 246 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:  3anidm12  1203  mob  2746  eqbrrdva  4533  funimaexglem  5010  fco  5084  f1oiso2  5494  caovimo  5722  smoel2  5949  nnaword  6115  3ecoptocl  6226  distrnq0  6615  addassnq0  6618  prcdnql  6640  prcunqu  6641  genpdisj  6679  cauappcvgprlemrnd  6806  caucvgprlemrnd  6829  caucvgprprlemrnd  6857  nn0n0n1ge2b  8378  fzind  8412  icoshft  8959  fzen  9009  shftuz  9646  ialgcvga  10273
  Copyright terms: Public domain W3C validator