Theorem imp43 433

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 427	. 2 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏))
3	2	imp 412	1 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  fundmen  9097  fiint  9356  ltexprlem6  11165  divgt0  12225  divge0  12226  le2sq2  14318  iscatd  17897  isfuncd  18090  islmodd  21192  lmodvsghm  21249  islssd  21261  basis2  23324  neindisj  23490  dvidlem  26290  spansneleq  32229  elspansn4  32232  adjmul  32751  kbass6  32780  mdsl0  32969  chirredlem1  33049  r1peuqusdeg1  36616  poimirlem29  38835  rngonegmn1r  39142  3dim1  40790  linepsubN  41075  pmapsub  41091  tgoldbach  49188