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

Theorem 3expib 1207
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 1203 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32impd 254 1 (𝜑 → ((𝜓𝜒) → 𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  w3a 979
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 981
This theorem is referenced by:  3anidm12  1305  mob  2931  eqbrrdva  4809  funimaexglem  5311  fco  5393  f1oiso2  5841  caovimo  6082  smoel2  6318  nnaword  6526  3ecoptocl  6638  sbthlemi10  6979  distrnq0  7472  addassnq0  7475  prcdnql  7497  prcunqu  7498  genpdisj  7536  cauappcvgprlemrnd  7663  caucvgprlemrnd  7686  caucvgprprlemrnd  7714  nn0n0n1ge2b  9346  fzind  9382  icoshft  10004  fzen  10057  seq3coll  10836  shftuz  10840  mulgcd  12031  algcvga  12065  lcmneg  12088  isnmgm  12798  issgrpd  12837  iscmnd  13192  unitmulclb  13419  rmodislmodlem  13596  rmodislmod  13597  blssps  14280  blss  14281  metcnp3  14364  sincosq1sgn  14600  sincosq2sgn  14601  sincosq3sgn  14602  sincosq4sgn  14603
  Copyright terms: Public domain W3C validator