Theorem imp42 432

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 424	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → (𝜃 → 𝜏))
3	2	imp 412	1 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜏)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  imp55  448  ltexprlem7  11134  fzdif1  13746  iscatd  17856  isposd  18505  pospropd  18508  mulgghm2  21791  ordtbaslem  23515  txbas  23895  nocvxminlem  28149  frgrncvvdeqlem8  30916  grporcan  31129  chirredlem1  33001  cvxpconn  36097  cvxsconn  36098  rngonegmn1l  38984  prnc  39110  reuopreuprim  48716  uhgrimisgrgriclem  49136