Theorem imp43 622

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

Syntax hints:   → wi 4   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  fundmen  8195  fiint  8402  ltexprlem6  10055  divgt0  11083  divge0  11084  le2sq2  13133  iscatd  16535  isfuncd  16726  islmodd  19071  lmodvsghm  19126  islssd  19138  basis2  20957  neindisj  21123  dvidlem  23878  spansneleq  28738  elspansn4  28741  adjmul  29260  kbass6  29289  mdsl0  29478  chirredlem1  29558  poimirlem29  33751  rngonegmn1r  34054  3dim1  35256  linepsubN  35541  pmapsub  35557  tgoldbach  42215  tgoldbachOLD  42222