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

Theorem 3exp1 1349
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 416 . 2 ((𝜑𝜓𝜒) → (𝜃𝜏))
323exp 1116 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  3an1rs  1356  funelss  7731  ltmpi  10313  cshf1  14163  lcmfunsnlem  15974  mulgaddcom  18242  mulginvcom  18243  symgfvne  18500  voliunlem3  24147  3cyclfrgrrn  28062  numclwwlk1lem2foa  28130  frgrregord013  28171  strlem3a  30026  hstrlem3a  30034  chirredlem1  30164  nn0prpwlem  33690  matunitlindflem1  34958  zerdivemp1x  35290  athgt  36657  paddasslem14  37034  paddidm  37042  tendospcanN  38224  jm2.26  39790  relexpxpmin  40265  0ellimcdiv  42148
  Copyright terms: Public domain W3C validator