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  3014  onmindif  6401  oaordex  8476  pssnn  9082  alephval3  10004  dfac5  10023  dfac2b  10025  coftr  10167  zorn2lem6  10395  addcanpi  10793  mulcanpi  10794  ltmpi  10798  ltexprlem6  10935  axpre-sup  11063  bndndx  12383  dmdprdd  19880  lssssr  20857  coe1fzgsumdlem  22188  evl1gsumdlem  22241  1stcrest  23338  upgrreslem  29249  umgrreslem  29250  mdsymlem3  32349  mdsymlem6  32352  sumdmdlem  32362  mclsax  35542  mclsppslem  35556  disjlem17  38777  prtlem17  38855  cvratlem  39400  paddidm  39820  pmodlem2  39826  pclfinclN  39929  onexoegt  43217  icceuelpart  47420