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

Theorem imp4c 416
 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 402 . 2 (𝜑 → ((𝜓𝜒) → (𝜃𝜏)))
32impd 402 1 (𝜑 → (((𝜓𝜒) ∧ 𝜃) → 𝜏))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 387 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 388 This theorem is referenced by:  imp44  421  imp5g  434  reuop  5982  omordi  7993  omwordri  7999  omass  8007  oewordri  8019  umgrclwwlkge2  27497  upgr4cycl4dv4e  27714  elspansn5  29132  atcvat3i  29954  mdsymlem5  29965  sumdmdlem  29976  cvrat4  36021  2reuimp  42718  sprsymrelfolem2  43021  reupr  43050
 Copyright terms: Public domain W3C validator