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  3021  onmindif  6417  oaordex  8493  pssnn  9103  alephval3  10032  dfac5  10051  dfac2b  10053  coftr  10195  zorn2lem6  10423  addcanpi  10822  mulcanpi  10823  ltmpi  10827  ltexprlem6  10964  axpre-sup  11092  bndndx  12436  dmdprdd  19976  lssssr  20949  coe1fzgsumdlem  22268  evl1gsumdlem  22321  1stcrest  23418  upgrreslem  29373  umgrreslem  29374  mdsymlem3  32476  mdsymlem6  32479  sumdmdlem  32489  mclsax  35751  mclsppslem  35765  disjlem17  39223  prtlem17  39322  cvratlem  39867  paddidm  40287  pmodlem2  40293  pclfinclN  40396  onexoegt  43672  icceuelpart  47896