Theorem imp43 429

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  fundmen  8856  fiint  9135  ltexprlem6  10843  divgt0  11889  divge0  11890  le2sq2  13900  iscatd  17427  isfuncd  17625  islmodd  20174  lmodvsghm  20229  islssd  20242  basis2  22146  neindisj  22313  dvidlem  25124  spansneleq  29977  elspansn4  29980  adjmul  30499  kbass6  30528  mdsl0  30717  chirredlem1  30797  poimirlem29  35850  rngonegmn1r  36144  3dim1  37523  linepsubN  37808  pmapsub  37824  tgoldbach  45327