Theorem imp43 430

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  fundmen  8585  fiint  8797  ltexprlem6  10465  divgt0  11510  divge0  11511  le2sq2  13503  iscatd  16946  isfuncd  17137  islmodd  19642  lmodvsghm  19697  islssd  19709  basis2  21561  neindisj  21727  dvidlem  24515  spansneleq  29349  elspansn4  29352  adjmul  29871  kbass6  29900  mdsl0  30089  chirredlem1  30169  poimirlem29  34923  rngonegmn1r  35222  3dim1  36605  linepsubN  36890  pmapsub  36906  tgoldbach  43989