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  3053  onmindif  6456  oaordex  8543  pssnn  9153  alephval3  10094  dfac5  10112  dfac2b  10114  coftr  10257  zorn2lem6  10485  addcanpi  10884  mulcanpi  10885  ltmpi  10889  ltexprlem6  11026  axpre-sup  11154  bndndx  12503  dmdprdd  20071  lssssr  21053  coe1fzgsumdlem  22432  evl1gsumdlem  22485  1stcrest  23579  upgrreslem  29595  umgrreslem  29596  mdsymlem3  32698  mdsymlem6  32701  sumdmdlem  32711  mclsax  35960  mclsppslem  35974  disjlem17  39441  prtlem17  39540  cvratlem  40085  paddidm  40505  pmodlem2  40511  pclfinclN  40614  onexoegt  43863  icceuelpart  48074