Theorem imp43 433

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  fundmen  9035  fiint  9293  ltexprlem6  11041  divgt0  12098  divge0  12099  le2sq2  14189  iscatd  17751  isfuncd  17944  islmodd  21037  lmodvsghm  21094  islssd  21106  basis2  23158  neindisj  23324  dvidlem  26125  spansneleq  31993  elspansn4  31996  adjmul  32515  kbass6  32544  mdsl0  32733  chirredlem1  32813  r1peuqusdeg1  36172  poimirlem29  38357  rngonegmn1r  38651  3dim1  40299  linepsubN  40584  pmapsub  40600  tgoldbach  48640