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  3019  onmindif  6409  oaordex  8483  pssnn  9091  alephval3  10018  dfac5  10037  dfac2b  10039  coftr  10181  zorn2lem6  10409  addcanpi  10808  mulcanpi  10809  ltmpi  10813  ltexprlem6  10950  axpre-sup  11078  bndndx  12398  dmdprdd  19928  lssssr  20903  coe1fzgsumdlem  22245  evl1gsumdlem  22298  1stcrest  23395  upgrreslem  29326  umgrreslem  29327  mdsymlem3  32429  mdsymlem6  32432  sumdmdlem  32442  mclsax  35712  mclsppslem  35726  disjlem17  38997  prtlem17  39075  cvratlem  39620  paddidm  40040  pmodlem2  40046  pclfinclN  40149  onexoegt  43428  icceuelpart  47624