Theorem imp4b 425

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  imp4a  426  imp43  431  imp5g  445  pm2.61da3ne  3046  onmindif  6440  oaordex  8527  pssnn  9137  alephval3  10066  dfac5  10085  dfac2b  10087  coftr  10230  zorn2lem6  10458  addcanpi  10857  mulcanpi  10858  ltmpi  10862  ltexprlem6  10999  axpre-sup  11127  bndndx  12480  dmdprdd  20041  lssssr  21021  coe1fzgsumdlem  22366  evl1gsumdlem  22419  1stcrest  23513  upgrreslem  29505  umgrreslem  29506  mdsymlem3  32608  mdsymlem6  32611  sumdmdlem  32621  mclsax  35919  mclsppslem  35933  disjlem17  39401  prtlem17  39500  cvratlem  40045  paddidm  40465  pmodlem2  40471  pclfinclN  40574  onexoegt  43821  icceuelpart  48042