Theorem imp43 431

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  fundmen  8566  fiint  8779  ltexprlem6  10452  divgt0  11497  divge0  11498  le2sq2  13496  iscatd  16936  isfuncd  17127  islmodd  19633  lmodvsghm  19688  islssd  19700  basis2  21556  neindisj  21722  dvidlem  24518  spansneleq  29353  elspansn4  29356  adjmul  29875  kbass6  29904  mdsl0  30093  chirredlem1  30173  poimirlem29  35086  rngonegmn1r  35380  3dim1  36763  linepsubN  37048  pmapsub  37064  tgoldbach  44335