Theorem imp4b 425

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  imp4a  426  imp43  431  imp5g  445  pm2.61da3ne  3076  onmindif  6248  oaordex  8167  pssnn  8720  alephval3  9521  dfac5  9539  dfac2b  9541  coftr  9684  zorn2lem6  9912  addcanpi  10310  mulcanpi  10311  ltmpi  10315  ltexprlem6  10452  axpre-sup  10580  bndndx  11884  dmdprdd  19114  lssssr  19718  coe1fzgsumdlem  20930  evl1gsumdlem  20980  1stcrest  22058  upgrreslem  27094  umgrreslem  27095  mdsymlem3  30188  mdsymlem6  30191  sumdmdlem  30201  mclsax  32929  mclsppslem  32943  prtlem17  36172  cvratlem  36717  paddidm  37137  pmodlem2  37143  pclfinclN  37246  icceuelpart  43953