Theorem imp42 427

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  imp55  443  ltexprlem7  10956  fzdif1  13550  iscatd  17630  isposd  18279  pospropd  18282  mulgghm2  21451  ordtbaslem  23171  txbas  23550  nocvxminlem  27764  frgrncvvdeqlem8  30394  grporcan  30607  chirredlem1  32479  cvxpconn  35470  cvxsconn  35471  rngonegmn1l  38308  prnc  38434  reuopreuprim  48001  uhgrimisgrgriclem  48421