Theorem imp4b 410

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

Syntax hints:   → wi 4   ∧ wa 384

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 198  df-an 385

This theorem is referenced by:  imp4a  411  imp43  416  pm2.61da3ne  3078  onmindif  6040  oaordex  7885  pssnn  8427  alephval3  9226  dfac5  9244  dfac2b  9246  dfac2OLD  9248  coftr  9390  zorn2lem6  9618  addcanpi  10016  mulcanpi  10017  ltmpi  10021  ltexprlem6  10158  axpre-sup  10285  bndndx  11578  relexpaddd  14037  dmdprdd  18620  lssssr  19179  lssssrOLD  19180  coe1fzgsumdlem  19899  evl1gsumdlem  19948  1stcrest  21491  upgrreslem  26435  umgrreslem  26436  mdsymlem3  29615  mdsymlem6  29618  sumdmdlem  29628  mclsax  31811  mclsppslem  31825  prtlem17  34674  cvratlem  35220  paddidm  35640  pmodlem2  35646  pclfinclN  35749  icceuelpart  41965