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

Theorem 3expib 1107
 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 1103 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32impd 242 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:  3anidm12  1192  mob  2723  eqbrrdva  4505  funimaexglem  4982  fco  5056  f1oiso2  5466  caovimo  5694  smoel2  5918  nnaword  6084  3ecoptocl  6195  distrnq0  6557  addassnq0  6560  prcdnql  6582  prcunqu  6583  genpdisj  6621  cauappcvgprlemrnd  6748  caucvgprlemrnd  6771  caucvgprprlemrnd  6799  nn0n0n1ge2b  8320  fzind  8353  icoshft  8858  fzen  8907  shftuz  9418  ialgcvga  9890
 Copyright terms: Public domain W3C validator