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  6414  oaordex  8499  pssnn  9109  alephval3  10039  dfac5  10058  dfac2b  10060  coftr  10202  zorn2lem6  10430  addcanpi  10828  mulcanpi  10829  ltmpi  10833  ltexprlem6  10970  axpre-sup  11098  bndndx  12417  dmdprdd  19907  lssssr  20836  coe1fzgsumdlem  22166  evl1gsumdlem  22219  1stcrest  23316  upgrreslem  29207  umgrreslem  29208  mdsymlem3  32307  mdsymlem6  32310  sumdmdlem  32320  mclsax  35529  mclsppslem  35543  disjlem17  38764  prtlem17  38842  cvratlem  39388  paddidm  39808  pmodlem2  39814  pclfinclN  39917  onexoegt  43206  icceuelpart  47410