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  9002  fiint  9277  fiintOLD  9278  ltexprlem6  10994  divgt0  12051  divge0  12052  le2sq2  14100  iscatd  17634  isfuncd  17827  islmodd  20772  lmodvsghm  20829  islssd  20841  basis2  22838  neindisj  23004  dvidlem  25816  spansneleq  31499  elspansn4  31502  adjmul  32021  kbass6  32050  mdsl0  32239  chirredlem1  32319  r1peuqusdeg1  35630  poimirlem29  37643  rngonegmn1r  37936  3dim1  39461  linepsubN  39746  pmapsub  39762  tgoldbach  47818