Theorem imp43 428

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  fundmen  8968  fiint  9227  ltexprlem6  10955  divgt0  12015  divge0  12016  le2sq2  14088  iscatd  17630  isfuncd  17823  islmodd  20856  lmodvsghm  20913  islssd  20925  basis2  22934  neindisj  23100  dvidlem  25900  spansneleq  31659  elspansn4  31662  adjmul  32181  kbass6  32210  mdsl0  32399  chirredlem1  32479  r1peuqusdeg1  35871  poimirlem29  38016  rngonegmn1r  38309  3dim1  39959  linepsubN  40244  pmapsub  40260  tgoldbach  48308