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  8956  fiint  9216  fiintOLD  9217  ltexprlem6  10935  divgt0  11993  divge0  11994  le2sq2  14042  iscatd  17579  isfuncd  17772  islmodd  20769  lmodvsghm  20826  islssd  20838  basis2  22836  neindisj  23002  dvidlem  25814  spansneleq  31514  elspansn4  31517  adjmul  32036  kbass6  32065  mdsl0  32254  chirredlem1  32334  r1peuqusdeg1  35620  poimirlem29  37633  rngonegmn1r  37926  3dim1  39450  linepsubN  39735  pmapsub  39751  tgoldbach  47805