Theorem imp4b 424

Description: An importation inference. (Contributed by NM, 26-Apr-1994.) Shorten imp4a 425. (Revised by Wolf Lammen, 19-Jul-2021.)

Hypothesis

Ref	Expression
imp4.1	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Assertion

Ref	Expression
imp4b	⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏))

Proof of Theorem imp4b

Step	Hyp	Ref	Expression
1		imp4.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
2	1	imp 409	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → (𝜃 → 𝜏)))
3	2	impd 413	1 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏))

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  imp4a  425  imp43  430  imp5g  444  pm2.61da3ne  3036  onmindif  6425  oaordex  8511  pssnn  9122  alephval3  10052  dfac5  10071  dfac2b  10073  coftr  10216  zorn2lem6  10444  addcanpi  10843  mulcanpi  10844  ltmpi  10848  ltexprlem6  10985  axpre-sup  11113  bndndx  12466  dmdprdd  20013  lssssr  20990  coe1fzgsumdlem  22335  evl1gsumdlem  22388  1stcrest  23482  upgrreslem  29440  umgrreslem  29441  mdsymlem3  32543  mdsymlem6  32546  sumdmdlem  32556  mclsax  35857  mclsppslem  35871  disjlem17  39339  prtlem17  39438  cvratlem  39983  paddidm  40403  pmodlem2  40409  pclfinclN  40512  onexoegt  43759  icceuelpart  47980