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  8972  fiint  9231  ltexprlem6  10958  divgt0  12018  divge0  12019  le2sq2  14091  iscatd  17633  isfuncd  17826  islmodd  20855  lmodvsghm  20912  islssd  20924  basis2  22929  neindisj  23095  dvidlem  25895  spansneleq  31659  elspansn4  31662  adjmul  32181  kbass6  32210  mdsl0  32399  chirredlem1  32479  r1peuqusdeg1  35844  poimirlem29  37987  rngonegmn1r  38280  3dim1  39930  linepsubN  40215  pmapsub  40231  tgoldbach  48308