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

Theorem imp42 426
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 418 . 2 ((𝜑 ∧ (𝜓𝜒)) → (𝜃𝜏))
32imp 406 1 (((𝜑 ∧ (𝜓𝜒)) ∧ 𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  imp55  442  ltexprlem7  11080  fzdif1  13642  iscatd  17718  isposd  18381  pospropd  18385  mulgghm2  21505  ordtbaslem  23212  txbas  23591  nocvxminlem  27837  frgrncvvdeqlem8  30335  grporcan  30547  chirredlem1  32419  cvxpconn  35227  cvxsconn  35228  rngonegmn1l  37928  prnc  38054  reuopreuprim  47451  uhgrimisgrgriclem  47836
  Copyright terms: Public domain W3C validator