Theorem imp4b 611

Description: An importation inference. (Contributed by NM, 26-Apr-1994.) Shorten imp4a 612. (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 196  df-an 385

This theorem is referenced by:  imp4a  612  imp43  619  pm2.61da3ne  2871  onmindif  5732  oaordex  7525  pssnn  8063  alephval3  8816  dfac5  8834  dfac2  8836  coftr  8978  zorn2lem6  9206  addcanpi  9600  mulcanpi  9601  ltmpi  9605  ltexprlem6  9742  axpre-sup  9869  bndndx  11168  relexpaddd  13642  dmdprdd  18221  lssssr  18774  coe1fzgsumdlem  19492  evl1gsumdlem  19541  1stcrest  21066  mdsymlem3  28648  mdsymlem6  28651  sumdmdlem  28661  mclsax  30720  mclsppslem  30734  prtlem17  33179  cvratlem  33725  paddidm  34145  pmodlem2  34151  pclfinclN  34254  icceuelpart  39974