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  9070  fiint  9364  fiintOLD  9365  ltexprlem6  11079  divgt0  12134  divge0  12135  le2sq2  14172  iscatd  17718  isfuncd  17916  islmodd  20881  lmodvsghm  20938  islssd  20951  basis2  22974  neindisj  23141  dvidlem  25965  spansneleq  31599  elspansn4  31602  adjmul  32121  kbass6  32150  mdsl0  32339  chirredlem1  32419  r1peuqusdeg1  35628  poimirlem29  37636  rngonegmn1r  37929  3dim1  39450  linepsubN  39735  pmapsub  39751  tgoldbach  47742