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  9005  fiint  9284  fiintOLD  9285  ltexprlem6  11001  divgt0  12058  divge0  12059  le2sq2  14107  iscatd  17641  isfuncd  17834  islmodd  20779  lmodvsghm  20836  islssd  20848  basis2  22845  neindisj  23011  dvidlem  25823  spansneleq  31506  elspansn4  31509  adjmul  32028  kbass6  32057  mdsl0  32246  chirredlem1  32326  r1peuqusdeg1  35637  poimirlem29  37650  rngonegmn1r  37943  3dim1  39468  linepsubN  39753  pmapsub  39769  tgoldbach  47822