Theorem imp4b 614

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

Syntax hints:   → wi 4   ∧ wa 383

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 385

This theorem is referenced by:  imp4a  615  imp43  622  pm2.61da3ne  3009  onmindif  5964  oaordex  7795  pssnn  8331  alephval3  9094  dfac5  9112  dfac2b  9114  dfac2OLD  9116  coftr  9258  zorn2lem6  9486  addcanpi  9884  mulcanpi  9885  ltmpi  9889  ltexprlem6  10026  axpre-sup  10153  bndndx  11454  relexpaddd  13964  dmdprdd  18569  lssssr  19126  coe1fzgsumdlem  19844  evl1gsumdlem  19893  1stcrest  21429  upgrreslem  26366  umgrreslem  26367  mdsymlem3  29544  mdsymlem6  29547  sumdmdlem  29557  mclsax  31744  mclsppslem  31758  prtlem17  34634  cvratlem  35179  paddidm  35599  pmodlem2  35605  pclfinclN  35708  icceuelpart  41851