Theorem imp4b 427

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  imp4a  428  imp43  433  imp5g  447  pm2.61da3ne  3044  onmindif  6452  oaordex  8546  pssnn  9164  alephval3  10114  dfac5  10132  dfac2b  10134  coftr  10276  zorn2lem6  10504  addcanpi  10909  mulcanpi  10910  ltmpi  10914  ltexprlem6  11051  axpre-sup  11179  bndndx  12528  dmdprdd  20129  lssssr  21139  coe1fzgsumdlem  22529  evl1gsumdlem  22582  1stcrest  23679  upgrreslem  29765  umgrreslem  29766  mdsymlem3  32887  mdsymlem6  32890  sumdmdlem  32900  mclsax  36149  mclsppslem  36163  disjlem17  39651  prtlem17  39750  cvratlem  40295  paddidm  40715  pmodlem2  40721  pclfinclN  40824  onexoegt  44086  icceuelpart  48337