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  8978  fiint  9237  ltexprlem6  10964  divgt0  12024  divge0  12025  le2sq2  14097  iscatd  17639  isfuncd  17832  islmodd  20861  lmodvsghm  20918  islssd  20930  basis2  22916  neindisj  23082  dvidlem  25882  spansneleq  31641  elspansn4  31644  adjmul  32163  kbass6  32192  mdsl0  32381  chirredlem1  32461  r1peuqusdeg1  35825  poimirlem29  37970  rngonegmn1r  38263  3dim1  39913  linepsubN  40198  pmapsub  40214  tgoldbach  48293