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

Theorem exp42 439
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 423 . 2 (𝜑 → ((𝜓𝜒) → (𝜃𝜏)))
32expd 419 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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
This theorem is referenced by:  isofrlem  7075  f1ocnv2d  7381  oelim  8142  zorn2lem7  9909  addid1  10805  initoeu1  17260  termoeu1  17267  issubg4  18287  lmodvsdir  19644  lmodvsass  19645  gsummatr01lem4  21253  dvfsumrlim3  24625  wwlksext2clwwlk  27831  shscli  29089  f1o3d  30369  slmdvsdir  30862  slmdvsass  30863  lshpcmp  36184
  Copyright terms: Public domain W3C validator