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  3045  onmindif  6457  oaordex  8566  pssnn  9184  alephval3  10189  dfac5  10207  dfac2b  10209  coftr  10351  zorn2lem6  10579  addcanpi  10984  mulcanpi  10985  ltmpi  10989  ltexprlem6  11126  axpre-sup  11254  bndndx  12605  dmdprdd  20215  lssssr  21229  coe1fzgsumdlem  22621  evl1gsumdlem  22674  1stcrest  23771  upgrreslem  29885  umgrreslem  29886  mdsymlem3  33007  mdsymlem6  33010  sumdmdlem  33020  mclsax  36334  mclsppslem  36348  disjlem17  39834  prtlem17  39933  cvratlem  40478  paddidm  40898  pmodlem2  40904  pclfinclN  41007  onexoegt  44245  icceuelpart  48517