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

Theorem 3exp1 1344
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 413 . 2 ((𝜑𝜓𝜒) → (𝜃𝜏))
323exp 1111 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  3an1rs  1351  funelss  7735  ltmpi  10314  cshf1  14160  lcmfunsnlem  15973  mulgaddcom  18189  mulginvcom  18190  symgfvne  18444  voliunlem3  24080  3cyclfrgrrn  27992  numclwwlk1lem2foa  28060  frgrregord013  28101  strlem3a  29956  hstrlem3a  29964  chirredlem1  30094  nn0prpwlem  33567  matunitlindflem1  34769  zerdivemp1x  35106  athgt  36472  paddasslem14  36849  paddidm  36857  tendospcanN  38039  jm2.26  39477  relexpxpmin  39940  0ellimcdiv  41806
  Copyright terms: Public domain W3C validator