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

Theorem imp42 427
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 419 . 2 ((𝜑 ∧ (𝜓𝜒)) → (𝜃𝜏))
32imp 407 1 (((𝜑 ∧ (𝜓𝜒)) ∧ 𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  imp55  443  ltexprlem7  10310  iscatd  16773  isposd  17394  pospropd  17573  mulgghm2  20326  ordtbaslem  21480  txbas  21859  frgrncvvdeqlem8  27777  grporcan  27986  chirredlem1  29858  cvxpconn  32097  cvxsconn  32098  nocvxminlem  32856  rngonegmn1l  34751  prnc  34877  reuopreuprim  43170
  Copyright terms: Public domain W3C validator