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

Theorem exp42 427
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 411 . 2 (𝜑 → ((𝜓𝜒) → (𝜃𝜏)))
32expd 405 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385
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 199  df-an 386
This theorem is referenced by:  isofrlem  6818  f1ocnv2d  7120  oelim  7854  zorn2lem7  9612  addid1  10506  initoeu1  16975  termoeu1  16982  issubg4  17926  lmodvsdir  19205  lmodvsass  19206  gsummatr01lem4  20791  dvfsumrlim3  24137  wwlksext2clwwlk  27373  shscli  28701  f1o3d  29950  slmdvsdir  30285  slmdvsass  30286  lshpcmp  35009
  Copyright terms: Public domain W3C validator