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  8968  fiint  9227  ltexprlem6  10952  divgt0  12010  divge0  12011  le2sq2  14058  iscatd  17596  isfuncd  17789  islmodd  20817  lmodvsghm  20874  islssd  20886  basis2  22895  neindisj  23061  dvidlem  25872  spansneleq  31645  elspansn4  31648  adjmul  32167  kbass6  32196  mdsl0  32385  chirredlem1  32465  r1peuqusdeg1  35837  poimirlem29  37850  rngonegmn1r  38143  3dim1  39727  linepsubN  40012  pmapsub  40028  tgoldbach  48063