Theorem imp43 414

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

Syntax hints:   → wi 4   ∧ wa 382

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 383

This theorem is referenced by:  fundmen  8187  fiint  8397  ltexprlem6  10069  divgt0  11097  divge0  11098  le2sq2  13146  iscatd  16541  isfuncd  16732  islmodd  19079  lmodvsghm  19134  islssd  19146  basis2  20976  neindisj  21142  dvidlem  23899  spansneleq  28769  elspansn4  28772  adjmul  29291  kbass6  29320  mdsl0  29509  chirredlem1  29589  poimirlem29  33771  rngonegmn1r  34073  3dim1  35276  linepsubN  35561  pmapsub  35577  tgoldbach  42230  tgoldbachOLD  42237