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

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

Proof of Theorem imp42
StepHypRef Expression
1 imp4.1 . . 3 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
21imp32 417 . 2 ((𝜑 ∧ (𝜓𝜒)) → (𝜃𝜏))
32imp 405 1 (((𝜑 ∧ (𝜓𝜒)) ∧ 𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394
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 395
This theorem is referenced by:  imp55  441  ltexprlem7  11076  iscatd  17681  isposd  18343  pospropd  18347  mulgghm2  21462  ordtbaslem  23180  txbas  23559  nocvxminlem  27804  frgrncvvdeqlem8  30236  grporcan  30448  chirredlem1  32320  cvxpconn  35083  cvxsconn  35084  rngonegmn1l  37655  prnc  37781  reuopreuprim  47134  uhgrimisgrgriclem  47513
  Copyright terms: Public domain W3C validator