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

Theorem 3expib 1201
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 1197 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32impd 252 1 (𝜑 → ((𝜓𝜒) → 𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 973
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 975
This theorem is referenced by:  3anidm12  1290  mob  2912  eqbrrdva  4781  funimaexglem  5281  fco  5363  f1oiso2  5806  caovimo  6046  smoel2  6282  nnaword  6490  3ecoptocl  6602  sbthlemi10  6943  distrnq0  7421  addassnq0  7424  prcdnql  7446  prcunqu  7447  genpdisj  7485  cauappcvgprlemrnd  7612  caucvgprlemrnd  7635  caucvgprprlemrnd  7663  nn0n0n1ge2b  9291  fzind  9327  icoshft  9947  fzen  9999  seq3coll  10777  shftuz  10781  mulgcd  11971  algcvga  12005  lcmneg  12028  isnmgm  12614  blssps  13221  blss  13222  metcnp3  13305  sincosq1sgn  13541  sincosq2sgn  13542  sincosq3sgn  13543  sincosq4sgn  13544
  Copyright terms: Public domain W3C validator