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  9027  fiint  9285  ltexprlem6  11025  divgt0  12082  divge0  12083  le2sq2  14170  iscatd  17728  isfuncd  17921  islmodd  20964  lmodvsghm  21021  islssd  21033  basis2  23076  neindisj  23242  dvidlem  26042  spansneleq  31862  elspansn4  31865  adjmul  32384  kbass6  32413  mdsl0  32602  chirredlem1  32682  r1peuqusdeg1  36033  poimirlem29  38187  rngonegmn1r  38480  3dim1  40130  linepsubN  40415  pmapsub  40431  tgoldbach  48470