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

Step	Hyp	Ref	Expression
1		imp4.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
2	1	imp32 422	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → (𝜃 → 𝜏))
3	2	imp 410	1 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜏)

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 209  df-an 400

This theorem is referenced by:  imp55  446  ltexprlem7  11000  fzdif1  13610  iscatd  17705  isposd  18354  pospropd  18357  mulgghm2  21528  ordtbaslem  23248  txbas  23627  nocvxminlem  27847  frgrncvvdeqlem8  30508  grporcan  30721  chirredlem1  32593  cvxpconn  35592  cvxsconn  35593  rngonegmn1l  38440  prnc  38566  reuopreuprim  48132  uhgrimisgrgriclem  48552