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  3048  onmindif  6483  oaordex  8604  pssnn  9222  alephval3  10228  dfac5  10246  dfac2b  10248  coftr  10390  zorn2lem6  10618  addcanpi  11023  mulcanpi  11024  ltmpi  11028  ltexprlem6  11165  axpre-sup  11293  bndndx  12645  dmdprdd  20266  lssssr  21280  coe1fzgsumdlem  22676  evl1gsumdlem  22729  1stcrest  23826  upgrreslem  29942  umgrreslem  29943  mdsymlem3  33064  mdsymlem6  33067  sumdmdlem  33077  mclsax  36542  mclsppslem  36556  disjlem17  40100  prtlem17  40199  cvratlem  40744  paddidm  41164  pmodlem2  41170  pclfinclN  41273  onexoegt  44507  icceuelpart  48791