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

Theorem imp42 428
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 420 . 2 ((𝜑 ∧ (𝜓𝜒)) → (𝜃𝜏))
32imp 408 1 (((𝜑 ∧ (𝜓𝜒)) ∧ 𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 398
This theorem is referenced by:  imp55  444  ltexprlem7  11037  iscatd  17617  isposd  18276  pospropd  18280  mulgghm2  21046  ordtbaslem  22692  txbas  23071  nocvxminlem  27279  frgrncvvdeqlem8  29590  grporcan  29802  chirredlem1  31674  cvxpconn  34264  cvxsconn  34265  rngonegmn1l  36857  prnc  36983  reuopreuprim  46242
  Copyright terms: Public domain W3C validator