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

Theorem imp42 621
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 448 . 2 ((𝜑 ∧ (𝜓𝜒)) → (𝜃𝜏))
32imp 444 1 (((𝜑 ∧ (𝜓𝜒)) ∧ 𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  imp55  628  ltexprlem7  10076  iscatd  16555  isposd  17176  pospropd  17355  mulgghm2  20067  ordtbaslem  21214  txbas  21592  frgrncvvdeqlem8  27481  grporcan  27702  chirredlem1  29579  cvxpconn  31552  cvxsconn  31553  nocvxminlem  32220  rngonegmn1l  34071  prnc  34197
  Copyright terms: Public domain W3C validator