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

This theorem is referenced by:  fundmen  9012  fiint  9271  ltexprlem6  10999  divgt0  12060  divge0  12061  le2sq2  14148  iscatd  17705  isfuncd  17898  islmodd  20930  lmodvsghm  20987  islssd  20999  basis2  23008  neindisj  23174  dvidlem  25974  spansneleq  31770  elspansn4  31773  adjmul  32292  kbass6  32321  mdsl0  32510  chirredlem1  32590  r1peuqusdeg1  35990  poimirlem29  38145  rngonegmn1r  38438  3dim1  40088  linepsubN  40373  pmapsub  40389  tgoldbach  48436