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  9045  fiint  9338  fiintOLD  9339  ltexprlem6  11055  divgt0  12110  divge0  12111  le2sq2  14153  iscatd  17685  isfuncd  17878  islmodd  20823  lmodvsghm  20880  islssd  20892  basis2  22889  neindisj  23055  dvidlem  25868  spansneleq  31551  elspansn4  31554  adjmul  32073  kbass6  32102  mdsl0  32291  chirredlem1  32371  r1peuqusdeg1  35665  poimirlem29  37673  rngonegmn1r  37966  3dim1  39486  linepsubN  39771  pmapsub  39787  tgoldbach  47831