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

Theorem 3exp2 1227
Description: Exportation from right triple conjunction. (Contributed by NM, 26-Oct-2006.)
Hypothesis
Ref Expression
3exp2.1 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜏)
Assertion
Ref Expression
3exp2 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))

Proof of Theorem 3exp2
StepHypRef Expression
1 3exp2.1 . . 3 ((𝜑 ∧ (𝜓𝜒𝜃)) → 𝜏)
21ex 115 . 2 (𝜑 → ((𝜓𝜒𝜃) → 𝜏))
323expd 1226 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  w3a 980
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 982
This theorem is referenced by:  3anassrs  1231  po2nr  4327  fliftfund  5819  tfrlemibxssdm  6353  tfr1onlembxssdm  6369  tfrcllembxssdm  6382  grpinveu  12997  grpid  12998  grpasscan1  13022  imasgrp2  13067  imasrng  13327  imasring  13431  islmodd  13626  islssmd  13692  mulgghm2  13923  isxmetd  14324  dvidlemap  14637
  Copyright terms: Public domain W3C validator