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

Theorem imp4c 427
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 414 . 2 (𝜑 → ((𝜓𝜒) → (𝜃𝜏)))
32impd 414 1 (𝜑 → (((𝜓𝜒) ∧ 𝜃) → 𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  imp44  432  reuop  6122  omordi  8179  omwordri  8185  omass  8193  oewordri  8205  umgrclwwlkge2  27774  upgr4cycl4dv4e  27968  elspansn5  29355  atcvat3i  30177  mdsymlem5  30188  sumdmdlem  30199  cvrat4  36698  2reuimp  43611  sprsymrelfolem2  43950  reupr  43979
  Copyright terms: Public domain W3C validator