Theorem imp4b 422

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  imp4a  423  imp43  428  imp5g  442  pm2.61da3ne  3031  onmindif  6456  oaordex  8557  pssnn  9167  pssnnOLD  9264  alephval3  10104  dfac5  10122  dfac2b  10124  coftr  10267  zorn2lem6  10495  addcanpi  10893  mulcanpi  10894  ltmpi  10898  ltexprlem6  11035  axpre-sup  11163  bndndx  12470  dmdprdd  19868  lssssr  20563  coe1fzgsumdlem  21824  evl1gsumdlem  21874  1stcrest  22956  upgrreslem  28558  umgrreslem  28559  mdsymlem3  31653  mdsymlem6  31656  sumdmdlem  31666  mclsax  34555  mclsppslem  34569  disjlem17  37664  prtlem17  37741  cvratlem  38287  paddidm  38707  pmodlem2  38713  pclfinclN  38816  onexoegt  41983  icceuelpart  46094