Theorem imp4b 426

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  imp4a  427  imp43  432  imp5g  446  pm2.61da3ne  3047  onmindif  6455  oaordex  8539  pssnn  9149  alephval3  10090  dfac5  10108  dfac2b  10110  coftr  10252  zorn2lem6  10480  addcanpi  10879  mulcanpi  10880  ltmpi  10884  ltexprlem6  11021  axpre-sup  11149  bndndx  12498  dmdprdd  20066  lssssr  21075  coe1fzgsumdlem  22463  evl1gsumdlem  22516  1stcrest  23610  upgrreslem  29654  umgrreslem  29655  mdsymlem3  32757  mdsymlem6  32760  sumdmdlem  32770  mclsax  36061  mclsppslem  36075  disjlem17  39571  prtlem17  39670  cvratlem  40215  paddidm  40635  pmodlem2  40641  pclfinclN  40744  onexoegt  43991  icceuelpart  48205