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  3017  onmindif  6395  oaordex  8468  pssnn  9073  alephval3  9996  dfac5  10015  dfac2b  10017  coftr  10159  zorn2lem6  10387  addcanpi  10785  mulcanpi  10786  ltmpi  10790  ltexprlem6  10927  axpre-sup  11055  bndndx  12375  dmdprdd  19908  lssssr  20882  coe1fzgsumdlem  22213  evl1gsumdlem  22266  1stcrest  23363  upgrreslem  29277  umgrreslem  29278  mdsymlem3  32377  mdsymlem6  32380  sumdmdlem  32390  mclsax  35605  mclsppslem  35619  disjlem17  38837  prtlem17  38915  cvratlem  39460  paddidm  39880  pmodlem2  39886  pclfinclN  39989  onexoegt  43277  icceuelpart  47467