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  17610  isfuncd  17803  islmodd  20748  lmodvsghm  20805  islssd  20817  basis2  22814  neindisj  22980  dvidlem  25792  spansneleq  31472  elspansn4  31475  adjmul  31994  kbass6  32023  mdsl0  32212  chirredlem1  32292  r1peuqusdeg1  35603  poimirlem29  37616  rngonegmn1r  37909  3dim1  39434  linepsubN  39719  pmapsub  39735  tgoldbach  47791