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  9038  fiint  9296  ltexprlem6  11050  divgt0  12107  divge0  12108  le2sq2  14199  iscatd  17761  isfuncd  17954  islmodd  21050  lmodvsghm  21107  islssd  21119  basis2  23176  neindisj  23342  dvidlem  26142  spansneleq  32051  elspansn4  32054  adjmul  32573  kbass6  32602  mdsl0  32791  chirredlem1  32871  r1peuqusdeg1  36222  poimirlem29  38398  rngonegmn1r  38692  3dim1  40340  linepsubN  40625  pmapsub  40641  tgoldbach  48733