Theorem imp43 427

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  fundmen  8953  fiint  9211  ltexprlem6  10932  divgt0  11990  divge0  11991  le2sq2  14042  iscatd  17579  isfuncd  17772  islmodd  20799  lmodvsghm  20856  islssd  20868  basis2  22866  neindisj  23032  dvidlem  25843  spansneleq  31550  elspansn4  31553  adjmul  32072  kbass6  32101  mdsl0  32290  chirredlem1  32370  r1peuqusdeg1  35687  poimirlem29  37699  rngonegmn1r  37992  3dim1  39576  linepsubN  39861  pmapsub  39877  tgoldbach  47927