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  9071  fiint  9366  fiintOLD  9367  ltexprlem6  11081  divgt0  12136  divge0  12137  le2sq2  14175  iscatd  17716  isfuncd  17910  islmodd  20864  lmodvsghm  20921  islssd  20933  basis2  22958  neindisj  23125  dvidlem  25950  spansneleq  31589  elspansn4  31592  adjmul  32111  kbass6  32140  mdsl0  32329  chirredlem1  32409  r1peuqusdeg1  35648  poimirlem29  37656  rngonegmn1r  37949  3dim1  39469  linepsubN  39754  pmapsub  39770  tgoldbach  47804