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

Theorem exp42 637
 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 628 . 2 (𝜑 → ((𝜓𝜒) → (𝜃𝜏)))
32expd 451 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383 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 196  df-an 385 This theorem is referenced by:  isofrlem  6490  f1ocnv2d  6784  oelim  7501  zorn2lem7  9207  addid1  10095  initoeu1  16484  termoeu1  16491  issubg4  17436  lmodvsdir  18710  lmodvsass  18711  gsummatr01lem4  20283  dvfsumrlim3  23600  shscli  27560  f1o3d  28813  slmdvsdir  29100  slmdvsass  29101  lshpcmp  33293
 Copyright terms: Public domain W3C validator