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  6372  oaordex  8420  pssnn  8989  pssnnOLD  9084  alephval3  9912  dfac5  9930  dfac2b  9932  coftr  10075  zorn2lem6  10303  addcanpi  10701  mulcanpi  10702  ltmpi  10706  ltexprlem6  10843  axpre-sup  10971  bndndx  12278  dmdprdd  19647  lssssr  20260  coe1fzgsumdlem  21517  evl1gsumdlem  21567  1stcrest  22649  upgrreslem  27716  umgrreslem  27717  mdsymlem3  30812  mdsymlem6  30815  sumdmdlem  30825  mclsax  33576  mclsppslem  33590  prtlem17  36932  cvratlem  37477  paddidm  37897  pmodlem2  37903  pclfinclN  38006  icceuelpart  44946