MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3exp1 Structured version   Visualization version   GIF version

Theorem 3exp1 1275
Description: Exportation from left triple conjunction. (Contributed by NM, 24-Feb-2005.)
Hypothesis
Ref Expression
3exp1.1 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜏)
Assertion
Ref Expression
3exp1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))

Proof of Theorem 3exp1
StepHypRef Expression
1 3exp1.1 . . 3 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜏)
21ex 449 . 2 ((𝜑𝜓𝜒) → (𝜃𝜏))
323exp 1256 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1031
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 196  df-an 385  df-3an 1033
This theorem is referenced by:  ltmpi  9583  cshf1  13356  lcmfunsnlem  15141  mulginvcom  17337  symgfvne  17580  voliunlem3  23072  frgraregord013  26439  strlem3a  28289  hstrlem3a  28297  chirredlem1  28427  nn0prpwlem  31281  matunitlindflem1  32369  zerdivemp1x  32710  athgt  33554  paddasslem14  33931  paddidm  33939  tendospcanN  35124  jm2.26  36381  relexpxpmin  36822  0ellimcdiv  38510  3cyclfrgrrn  41448  av-frgraregord013  41541
  Copyright terms: Public domain W3C validator