Theorem imp4b 612

Description: An importation inference. (Contributed by NM, 26-Apr-1994.) Shorten imp4a 613. (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 445	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → (𝜃 → 𝜏)))
3	2	impd 447	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 197  df-an 386

This theorem is referenced by:  imp4a  613  imp43  620  pm2.61da3ne  2879  onmindif  5784  oaordex  7598  pssnn  8138  alephval3  8893  dfac5  8911  dfac2  8913  coftr  9055  zorn2lem6  9283  addcanpi  9681  mulcanpi  9682  ltmpi  9686  ltexprlem6  9823  axpre-sup  9950  bndndx  11251  relexpaddd  13744  dmdprdd  18338  lssssr  18893  coe1fzgsumdlem  19611  evl1gsumdlem  19660  1stcrest  21196  mdsymlem3  29152  mdsymlem6  29155  sumdmdlem  29165  mclsax  31227  mclsppslem  31241  prtlem17  33680  cvratlem  34226  paddidm  34646  pmodlem2  34652  pclfinclN  34755  icceuelpart  40700