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  3021  onmindif  6411  oaordex  8485  pssnn  9093  alephval3  10020  dfac5  10039  dfac2b  10041  coftr  10183  zorn2lem6  10411  addcanpi  10810  mulcanpi  10811  ltmpi  10815  ltexprlem6  10952  axpre-sup  11080  bndndx  12400  dmdprdd  19930  lssssr  20905  coe1fzgsumdlem  22247  evl1gsumdlem  22300  1stcrest  23397  upgrreslem  29377  umgrreslem  29378  mdsymlem3  32480  mdsymlem6  32483  sumdmdlem  32493  mclsax  35763  mclsppslem  35777  disjlem17  39058  prtlem17  39136  cvratlem  39681  paddidm  40101  pmodlem2  40107  pclfinclN  40210  onexoegt  43486  icceuelpart  47682