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  3015  onmindif  6429  oaordex  8525  pssnn  9138  alephval3  10070  dfac5  10089  dfac2b  10091  coftr  10233  zorn2lem6  10461  addcanpi  10859  mulcanpi  10860  ltmpi  10864  ltexprlem6  11001  axpre-sup  11129  bndndx  12448  dmdprdd  19938  lssssr  20867  coe1fzgsumdlem  22197  evl1gsumdlem  22250  1stcrest  23347  upgrreslem  29238  umgrreslem  29239  mdsymlem3  32341  mdsymlem6  32344  sumdmdlem  32354  mclsax  35563  mclsppslem  35577  disjlem17  38798  prtlem17  38876  cvratlem  39422  paddidm  39842  pmodlem2  39848  pclfinclN  39951  onexoegt  43240  icceuelpart  47441