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  9096  fiint  9394  fiintOLD  9395  ltexprlem6  11110  divgt0  12163  divge0  12164  le2sq2  14185  iscatd  17731  isfuncd  17929  islmodd  20886  lmodvsghm  20943  islssd  20956  basis2  22979  neindisj  23146  dvidlem  25970  spansneleq  31602  elspansn4  31605  adjmul  32124  kbass6  32153  mdsl0  32342  chirredlem1  32422  r1peuqusdeg1  35611  poimirlem29  37609  rngonegmn1r  37902  3dim1  39424  linepsubN  39709  pmapsub  39725  tgoldbach  47691