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

Theorem 3expib 1188
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 1184 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32impd 252 1 (𝜑 → ((𝜓𝜒) → 𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 963
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 965
This theorem is referenced by:  3anidm12  1277  mob  2894  eqbrrdva  4756  funimaexglem  5253  fco  5335  f1oiso2  5777  caovimo  6014  smoel2  6250  nnaword  6458  3ecoptocl  6569  sbthlemi10  6910  distrnq0  7379  addassnq0  7382  prcdnql  7404  prcunqu  7405  genpdisj  7443  cauappcvgprlemrnd  7570  caucvgprlemrnd  7593  caucvgprprlemrnd  7621  nn0n0n1ge2b  9243  fzind  9279  icoshft  9894  fzen  9945  seq3coll  10713  shftuz  10717  mulgcd  11900  algcvga  11928  lcmneg  11951  blssps  12838  blss  12839  metcnp3  12922  sincosq1sgn  13158  sincosq2sgn  13159  sincosq3sgn  13160  sincosq4sgn  13161
  Copyright terms: Public domain W3C validator