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

Theorem 3exp1 1305
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 1283 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 197  df-an 385  df-3an 1056
This theorem is referenced by:  3an1rs  1312  ltmpi  9764  cshf1  13602  lcmfunsnlem  15401  mulginvcom  17612  symgfvne  17854  voliunlem3  23366  3cyclfrgrrn  27266  numclwlk1lem2foa  27344  frgrregord013  27382  strlem3a  29239  hstrlem3a  29247  chirredlem1  29377  nn0prpwlem  32442  matunitlindflem1  33535  zerdivemp1x  33876  athgt  35060  paddasslem14  35437  paddidm  35445  tendospcanN  36629  jm2.26  37886  relexpxpmin  38326  0ellimcdiv  40199
  Copyright terms: Public domain W3C validator