Theorem imp43 432

Description: An importation inference. (Contributed by NM, 26-Apr-1994.)

Hypothesis

Ref	Expression
imp4.1	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Assertion

Ref	Expression
imp43	⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)

Proof of Theorem imp43

Step	Hyp	Ref	Expression
1		imp4.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
2	1	imp4b 426	. 2 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏))
3	2	imp 411	1 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  fundmen  9024  fiint  9282  ltexprlem6  11021  divgt0  12078  divge0  12079  le2sq2  14167  iscatd  17724  isfuncd  17917  islmodd  20987  lmodvsghm  21044  islssd  21056  basis2  23108  neindisj  23274  dvidlem  26074  spansneleq  31922  elspansn4  31925  adjmul  32444  kbass6  32473  mdsl0  32662  chirredlem1  32742  r1peuqusdeg1  36135  poimirlem29  38300  rngonegmn1r  38593  3dim1  40241  linepsubN  40526  pmapsub  40542  tgoldbach  48582