Theorem imp4b 427

Description: An importation inference. (Contributed by NM, 26-Apr-1994.) Shorten imp4a 428. (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 412	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → (𝜃 → 𝜏)))
3	2	impd 416	1 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  imp4a  428  imp43  433  imp5g  447  pm2.61da3ne  3049  onmindif  6459  oaordex  8549  pssnn  9160  alephval3  10110  dfac5  10128  dfac2b  10130  coftr  10272  zorn2lem6  10500  addcanpi  10901  mulcanpi  10902  ltmpi  10906  ltexprlem6  11043  axpre-sup  11171  bndndx  12520  dmdprdd  20117  lssssr  21127  coe1fzgsumdlem  22515  evl1gsumdlem  22568  1stcrest  23662  upgrreslem  29714  umgrreslem  29715  mdsymlem3  32830  mdsymlem6  32833  sumdmdlem  32843  mclsax  36100  mclsppslem  36114  disjlem17  39611  prtlem17  39710  cvratlem  40255  paddidm  40675  pmodlem2  40681  pclfinclN  40784  onexoegt  44031  icceuelpart  48245