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

Theorem imp42 415
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 407 . 2 ((𝜑 ∧ (𝜓𝜒)) → (𝜃𝜏))
32imp 395 1 (((𝜑 ∧ (𝜓𝜒)) ∧ 𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 198  df-an 385
This theorem is referenced by:  imp55  431  ltexprlem7  10158  iscatd  16557  isposd  17179  pospropd  17358  mulgghm2  20072  ordtbaslem  21226  txbas  21604  frgrncvvdeqlem8  27503  grporcan  27723  chirredlem1  29599  cvxpconn  31568  cvxsconn  31569  nocvxminlem  32235  rngonegmn1l  34069  prnc  34195
  Copyright terms: Public domain W3C validator