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  9052  fiint  9311  ltexprlem6  11119  divgt0  12178  divge0  12179  le2sq2  14271  iscatd  17840  isfuncd  18033  islmodd  21134  lmodvsghm  21191  islssd  21203  basis2  23262  neindisj  23428  dvidlem  26228  spansneleq  32165  elspansn4  32168  adjmul  32687  kbass6  32716  mdsl0  32905  chirredlem1  32985  r1peuqusdeg1  36387  poimirlem29  38547  rngonegmn1r  38856  3dim1  40504  linepsubN  40789  pmapsub  40805  tgoldbach  48884