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

Theorem imp42 618
 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 196  df-an 385 This theorem is referenced by:  imp55  625  ltexprlem7  9743  iscatd  16157  isposd  16778  pospropd  16957  mulgghm2  19664  ordtbaslem  20802  txbas  21180  grporcan  26756  chirredlem1  28633  cvxpcon  30478  cvxscon  30479  nocvxminlem  31089  rngonegmn1l  32910  prnc  33036
 Copyright terms: Public domain W3C validator