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  3022  onmindif  6419  oaordex  8495  pssnn  9105  alephval3  10032  dfac5  10051  dfac2b  10053  coftr  10195  zorn2lem6  10423  addcanpi  10822  mulcanpi  10823  ltmpi  10827  ltexprlem6  10964  axpre-sup  11092  bndndx  12412  dmdprdd  19942  lssssr  20917  coe1fzgsumdlem  22259  evl1gsumdlem  22312  1stcrest  23409  upgrreslem  29389  umgrreslem  29390  mdsymlem3  32493  mdsymlem6  32496  sumdmdlem  32506  mclsax  35785  mclsppslem  35799  disjlem17  39153  prtlem17  39252  cvratlem  39797  paddidm  40217  pmodlem2  40223  pclfinclN  40326  onexoegt  43601  icceuelpart  47796