Theorem imp43 416

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

Syntax hints:   → wi 4   ∧ wa 384

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 198  df-an 385

This theorem is referenced by:  fundmen  8266  fiint  8476  ltexprlem6  10148  divgt0  11176  divge0  11177  le2sq2  13162  iscatd  16538  isfuncd  16729  islmodd  19073  lmodvsghm  19128  islssd  19140  basis2  20969  neindisj  21135  dvidlem  23893  spansneleq  28757  elspansn4  28760  adjmul  29279  kbass6  29308  mdsl0  29497  chirredlem1  29577  poimirlem29  33751  rngonegmn1r  34052  3dim1  35247  linepsubN  35532  pmapsub  35548  tgoldbach  42280