Theorem imp43 429

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  fundmen  9031  fiint  9324  ltexprlem6  11036  divgt0  12082  divge0  12083  le2sq2  14100  iscatd  17617  isfuncd  17815  islmodd  20477  lmodvsghm  20533  islssd  20546  basis2  22454  neindisj  22621  dvidlem  25432  spansneleq  30823  elspansn4  30826  adjmul  31345  kbass6  31374  mdsl0  31563  chirredlem1  31643  poimirlem29  36517  rngonegmn1r  36810  3dim1  38338  linepsubN  38623  pmapsub  38639  tgoldbach  46485