Theorem imp43 433

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  fundmen  9066  fiint  9325  ltexprlem6  11133  divgt0  12192  divge0  12193  le2sq2  14285  iscatd  17856  isfuncd  18049  islmodd  21150  lmodvsghm  21207  islssd  21219  basis2  23278  neindisj  23444  dvidlem  26244  spansneleq  32181  elspansn4  32184  adjmul  32703  kbass6  32732  mdsl0  32921  chirredlem1  33001  r1peuqusdeg1  36498  poimirlem29  38676  rngonegmn1r  38985  3dim1  40633  linepsubN  40918  pmapsub  40934  tgoldbach  49023