Theorem imp4b 421

Description: An importation inference. (Contributed by NM, 26-Apr-1994.) Shorten imp4a 422. (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 406	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → (𝜃 → 𝜏)))
3	2	impd 410	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:  imp4a  422  imp43  427  imp5g  441  pm2.61da3ne  3037  onmindif  6487  oaordex  8614  pssnn  9234  alephval3  10179  dfac5  10198  dfac2b  10200  coftr  10342  zorn2lem6  10570  addcanpi  10968  mulcanpi  10969  ltmpi  10973  ltexprlem6  11110  axpre-sup  11238  bndndx  12552  dmdprdd  20043  lssssr  20975  coe1fzgsumdlem  22328  evl1gsumdlem  22381  1stcrest  23482  upgrreslem  29339  umgrreslem  29340  mdsymlem3  32437  mdsymlem6  32440  sumdmdlem  32450  mclsax  35537  mclsppslem  35551  disjlem17  38755  prtlem17  38832  cvratlem  39378  paddidm  39798  pmodlem2  39804  pclfinclN  39907  onexoegt  43205  icceuelpart  47310