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

Theorem imp4c 424
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 411 . 2 (𝜑 → ((𝜓𝜒) → (𝜃𝜏)))
32impd 411 1 (𝜑 → (((𝜓𝜒) ∧ 𝜃) → 𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  imp44  429  reuop  6137  omordi  8181  omwordri  8187  omass  8195  oewordri  8207  umgrclwwlkge2  27696  upgr4cycl4dv4e  27891  elspansn5  29278  atcvat3i  30100  mdsymlem5  30111  sumdmdlem  30122  cvrat4  36459  2reuimp  43191  sprsymrelfolem2  43532  reupr  43561
  Copyright terms: Public domain W3C validator