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  8980  fiint  9239  ltexprlem6  10964  divgt0  12022  divge0  12023  le2sq2  14070  iscatd  17608  isfuncd  17801  islmodd  20829  lmodvsghm  20886  islssd  20898  basis2  22907  neindisj  23073  dvidlem  25884  spansneleq  31658  elspansn4  31661  adjmul  32180  kbass6  32209  mdsl0  32398  chirredlem1  32478  r1peuqusdeg1  35859  poimirlem29  37900  rngonegmn1r  38193  3dim1  39843  linepsubN  40128  pmapsub  40144  tgoldbach  48177