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

This theorem is referenced by:  imp4a  422  imp43  427  imp5g  441  pm2.61da3ne  3035  onmindif  6352  oaordex  8365  pssnn  8916  pssnnOLD  9001  alephval3  9850  dfac5  9868  dfac2b  9870  coftr  10013  zorn2lem6  10241  addcanpi  10639  mulcanpi  10640  ltmpi  10644  ltexprlem6  10781  axpre-sup  10909  bndndx  12215  dmdprdd  19583  lssssr  20196  coe1fzgsumdlem  21453  evl1gsumdlem  21503  1stcrest  22585  upgrreslem  27652  umgrreslem  27653  mdsymlem3  30746  mdsymlem6  30749  sumdmdlem  30759  mclsax  33510  mclsppslem  33524  prtlem17  36869  cvratlem  37414  paddidm  37834  pmodlem2  37840  pclfinclN  37943  icceuelpart  44840