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

Theorem imp4c 423
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 410 . 2 (𝜑 → ((𝜓𝜒) → (𝜃𝜏)))
32impd 410 1 (𝜑 → (((𝜓𝜒) ∧ 𝜃) → 𝜏))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  imp44  428  reuop  6312  omordi  8605  omwordri  8611  omass  8619  oewordri  8631  umgrclwwlkge2  30011  upgr4cycl4dv4e  30205  elspansn5  31594  atcvat3i  32416  mdsymlem5  32427  sumdmdlem  32438  cvrat4  39446  2reuimp  47132  sprsymrelfolem2  47485  reupr  47514  grtriprop  47913  isubgr3stgrlem6  47943
  Copyright terms: Public domain W3C validator