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

Theorem imp4c 425
Description: An importation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
imp4.1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Assertion
Ref Expression
imp4c (𝜑 → (((𝜓𝜒) ∧ 𝜃) → 𝜏))

Proof of Theorem imp4c
StepHypRef Expression
1 imp4.1 . . 3 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
21impd 412 . 2 (𝜑 → ((𝜓𝜒) → (𝜃𝜏)))
32impd 412 1 (𝜑 → (((𝜓𝜒) ∧ 𝜃) → 𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 398
This theorem is referenced by:  imp44  430  reuop  6293  omordi  8566  omwordri  8572  omass  8580  oewordri  8592  umgrclwwlkge2  29244  upgr4cycl4dv4e  29438  elspansn5  30827  atcvat3i  31649  mdsymlem5  31660  sumdmdlem  31671  cvrat4  38314  2reuimp  45823  sprsymrelfolem2  46161  reupr  46190
  Copyright terms: Public domain W3C validator