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  9041  fiint  9299  ltexprlem6  11053  divgt0  12110  divge0  12111  le2sq2  14202  iscatd  17764  isfuncd  17957  islmodd  21053  lmodvsghm  21110  islssd  21122  basis2  23179  neindisj  23345  dvidlem  26145  spansneleq  32054  elspansn4  32057  adjmul  32576  kbass6  32605  mdsl0  32794  chirredlem1  32874  r1peuqusdeg1  36225  poimirlem29  38401  rngonegmn1r  38695  3dim1  40343  linepsubN  40628  pmapsub  40644  tgoldbach  48736