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  8979  fiint  9253  fiintOLD  9254  ltexprlem6  10970  divgt0  12027  divge0  12028  le2sq2  14076  iscatd  17614  isfuncd  17807  islmodd  20804  lmodvsghm  20861  islssd  20873  basis2  22871  neindisj  23037  dvidlem  25849  spansneleq  31549  elspansn4  31552  adjmul  32071  kbass6  32100  mdsl0  32289  chirredlem1  32369  r1peuqusdeg1  35623  poimirlem29  37636  rngonegmn1r  37929  3dim1  39454  linepsubN  39739  pmapsub  39755  tgoldbach  47811