Theorem imp42 428

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  imp55  444  ltexprlem7  11037  iscatd  17617  isposd  18276  pospropd  18280  mulgghm2  21046  ordtbaslem  22692  txbas  23071  nocvxminlem  27279  frgrncvvdeqlem8  29559  grporcan  29771  chirredlem1  31643  cvxpconn  34233  cvxsconn  34234  rngonegmn1l  36809  prnc  36935  reuopreuprim  46194