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  7341  f1ocnv2d  7663  oelim  8538  zorn2lem7  10501  addrid  11400  initoeu1  17967  termoeu1  17974  issubg4  19063  lmodvsdir  20642  lmodvsass  20643  gsummatr01lem4  22382  dvfsumrlim3  25784  wwlksext2clwwlk  29575  shscli  30835  f1o3d  32116  slmdvsdir  32629  slmdvsass  32630  lshpcmp  38163
  Copyright terms: Public domain W3C validator