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  6446  oaordex  8570  pssnn  9182  alephval3  10124  dfac5  10143  dfac2b  10145  coftr  10287  zorn2lem6  10515  addcanpi  10913  mulcanpi  10914  ltmpi  10918  ltexprlem6  11055  axpre-sup  11183  bndndx  12500  dmdprdd  19982  lssssr  20911  coe1fzgsumdlem  22241  evl1gsumdlem  22294  1stcrest  23391  upgrreslem  29283  umgrreslem  29284  mdsymlem3  32386  mdsymlem6  32389  sumdmdlem  32399  mclsax  35591  mclsppslem  35605  disjlem17  38817  prtlem17  38894  cvratlem  39440  paddidm  39860  pmodlem2  39866  pclfinclN  39969  onexoegt  43268  icceuelpart  47450