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  3029  onmindif  6478  oaordex  8595  pssnn  9207  alephval3  10148  dfac5  10167  dfac2b  10169  coftr  10311  zorn2lem6  10539  addcanpi  10937  mulcanpi  10938  ltmpi  10942  ltexprlem6  11079  axpre-sup  11207  bndndx  12523  dmdprdd  20034  lssssr  20970  coe1fzgsumdlem  22323  evl1gsumdlem  22376  1stcrest  23477  upgrreslem  29336  umgrreslem  29337  mdsymlem3  32434  mdsymlem6  32437  sumdmdlem  32447  mclsax  35554  mclsppslem  35568  disjlem17  38781  prtlem17  38858  cvratlem  39404  paddidm  39824  pmodlem2  39830  pclfinclN  39933  onexoegt  43233  icceuelpart  47361