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  3109  onmindif  6283  oaordex  8187  pssnn  8739  alephval3  9539  dfac5  9557  dfac2b  9559  coftr  9698  zorn2lem6  9926  addcanpi  10324  mulcanpi  10325  ltmpi  10329  ltexprlem6  10466  axpre-sup  10594  bndndx  11899  relexpaddd  14416  dmdprdd  19124  lssssr  19728  coe1fzgsumdlem  20472  evl1gsumdlem  20522  1stcrest  22064  upgrreslem  27089  umgrreslem  27090  mdsymlem3  30185  mdsymlem6  30188  sumdmdlem  30198  mclsax  32820  mclsppslem  32834  prtlem17  36016  cvratlem  36561  paddidm  36981  pmodlem2  36987  pclfinclN  37090  icceuelpart  43603