Theorem imp4b 423

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  imp4a  424  imp43  429  imp5g  443  pm2.61da3ne  3032  onmindif  6457  oaordex  8558  pssnn  9168  pssnnOLD  9265  alephval3  10105  dfac5  10123  dfac2b  10125  coftr  10268  zorn2lem6  10496  addcanpi  10894  mulcanpi  10895  ltmpi  10899  ltexprlem6  11036  axpre-sup  11164  bndndx  12471  dmdprdd  19869  lssssr  20564  coe1fzgsumdlem  21825  evl1gsumdlem  21875  1stcrest  22957  upgrreslem  28592  umgrreslem  28593  mdsymlem3  31689  mdsymlem6  31692  sumdmdlem  31702  mclsax  34591  mclsppslem  34605  disjlem17  37717  prtlem17  37794  cvratlem  38340  paddidm  38760  pmodlem2  38766  pclfinclN  38869  onexoegt  42041  icceuelpart  46152