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  3014  onmindif  6426  oaordex  8522  pssnn  9132  alephval3  10063  dfac5  10082  dfac2b  10084  coftr  10226  zorn2lem6  10454  addcanpi  10852  mulcanpi  10853  ltmpi  10857  ltexprlem6  10994  axpre-sup  11122  bndndx  12441  dmdprdd  19931  lssssr  20860  coe1fzgsumdlem  22190  evl1gsumdlem  22243  1stcrest  23340  upgrreslem  29231  umgrreslem  29232  mdsymlem3  32334  mdsymlem6  32337  sumdmdlem  32347  mclsax  35556  mclsppslem  35570  disjlem17  38791  prtlem17  38869  cvratlem  39415  paddidm  39835  pmodlem2  39841  pclfinclN  39944  onexoegt  43233  icceuelpart  47437