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

Theorem exp42 435
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 419 . 2 (𝜑 → ((𝜓𝜒) → (𝜃𝜏)))
32expd 415 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  isofrlem  7360  f1ocnv2d  7686  oelim  8572  zorn2lem7  10542  addrid  11441  initoeu1  18056  termoeu1  18063  issubg4  19163  lmodvsdir  20884  lmodvsass  20885  gsummatr01lem4  22664  dvfsumrlim3  26074  wwlksext2clwwlk  30076  shscli  31336  f1o3d  32637  slmdvsdir  33222  slmdvsass  33223  lshpcmp  38989  relpfrlem  44974
  Copyright terms: Public domain W3C validator