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  3022  onmindif  6412  oaordex  8487  pssnn  9097  alephval3  10026  dfac5  10045  dfac2b  10047  coftr  10189  zorn2lem6  10417  addcanpi  10816  mulcanpi  10817  ltmpi  10821  ltexprlem6  10958  axpre-sup  11086  bndndx  12430  dmdprdd  19970  lssssr  20943  coe1fzgsumdlem  22281  evl1gsumdlem  22334  1stcrest  23431  upgrreslem  29390  umgrreslem  29391  mdsymlem3  32494  mdsymlem6  32497  sumdmdlem  32507  mclsax  35770  mclsppslem  35784  disjlem17  39240  prtlem17  39339  cvratlem  39884  paddidm  40304  pmodlem2  40310  pclfinclN  40413  onexoegt  43693  icceuelpart  47911