Theorem imp43 426

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

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  fundmen  9056  fiint  9350  ltexprlem6  11066  divgt0  12115  divge0  12116  le2sq2  14135  iscatd  17656  isfuncd  17854  islmodd  20761  lmodvsghm  20818  islssd  20831  basis2  22898  neindisj  23065  dvidlem  25888  spansneleq  31452  elspansn4  31455  adjmul  31974  kbass6  32003  mdsl0  32192  chirredlem1  32272  poimirlem29  37253  rngonegmn1r  37546  3dim1  39070  linepsubN  39355  pmapsub  39371  tgoldbach  47294