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  28561  umgrreslem  28562  mdsymlem3  31658  mdsymlem6  31661  sumdmdlem  31671  mclsax  34560  mclsppslem  34574  disjlem17  37669  prtlem17  37746  cvratlem  38292  paddidm  38712  pmodlem2  38718  pclfinclN  38821  onexoegt  41993  icceuelpart  46104