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

Theorem exp42 434
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
exp42.1 (((𝜑 ∧ (𝜓𝜒)) ∧ 𝜃) → 𝜏)
Assertion
Ref Expression
exp42 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))

Proof of Theorem exp42
StepHypRef Expression
1 exp42.1 . . 3 (((𝜑 ∧ (𝜓𝜒)) ∧ 𝜃) → 𝜏)
21exp31 418 . 2 (𝜑 → ((𝜓𝜒) → (𝜃𝜏)))
32expd 414 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394
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 206  df-an 395
This theorem is referenced by:  isofrlem  7352  f1ocnv2d  7679  oelim  8564  zorn2lem7  10545  addrid  11444  initoeu1  18033  termoeu1  18040  issubg4  19139  lmodvsdir  20862  lmodvsass  20863  gsummatr01lem4  22651  dvfsumrlim3  26059  wwlksext2clwwlk  29990  shscli  31250  f1o3d  32544  slmdvsdir  33080  slmdvsass  33081  lshpcmp  38686
  Copyright terms: Public domain W3C validator