Theorem imp4b 420

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  imp4a  421  imp43  426  imp5g  440  pm2.61da3ne  3020  onmindif  6463  oaordex  8579  pssnn  9196  pssnnOLD  9293  alephval3  10140  dfac5  10158  dfac2b  10160  coftr  10303  zorn2lem6  10531  addcanpi  10929  mulcanpi  10930  ltmpi  10934  ltexprlem6  11071  axpre-sup  11199  bndndx  12509  dmdprdd  19973  lssssr  20855  coe1fzgsumdlem  22252  evl1gsumdlem  22305  1stcrest  23406  upgrreslem  29194  umgrreslem  29195  mdsymlem3  32292  mdsymlem6  32295  sumdmdlem  32305  mclsax  35312  mclsppslem  35326  disjlem17  38403  prtlem17  38480  cvratlem  39026  paddidm  39446  pmodlem2  39452  pclfinclN  39555  onexoegt  42816  icceuelpart  46915