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  8966  fiint  9225  ltexprlem6  10950  divgt0  12008  divge0  12009  le2sq2  14056  iscatd  17594  isfuncd  17787  islmodd  20815  lmodvsghm  20872  islssd  20884  basis2  22893  neindisj  23059  dvidlem  25870  spansneleq  31594  elspansn4  31597  adjmul  32116  kbass6  32145  mdsl0  32334  chirredlem1  32414  r1peuqusdeg1  35786  poimirlem29  37789  rngonegmn1r  38082  3dim1  39666  linepsubN  39951  pmapsub  39967  tgoldbach  48005