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

Theorem imp42 430
 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 422 . 2 ((𝜑 ∧ (𝜓𝜒)) → (𝜃𝜏))
32imp 410 1 (((𝜑 ∧ (𝜓𝜒)) ∧ 𝜃) → 𝜏)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  imp55  446  ltexprlem7  10471  iscatd  16956  isposd  17577  pospropd  17756  mulgghm2  20212  ordtbaslem  21834  txbas  22213  frgrncvvdeqlem8  28135  grporcan  28345  chirredlem1  30217  cvxpconn  32668  cvxsconn  32669  nocvxminlem  33459  rngonegmn1l  35530  prnc  35656  reuopreuprim  44211
 Copyright terms: Public domain W3C validator