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  10844  iscatd  17427  isposd  18086  pospropd  18090  mulgghm2  20743  ordtbaslem  22384  txbas  22763  frgrncvvdeqlem8  28715  grporcan  28925  chirredlem1  30797  cvxpconn  33249  cvxsconn  33250  nocvxminlem  34017  rngonegmn1l  36143  prnc  36269  reuopreuprim  45036