Theorem imp4b 427

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  imp4a  428  imp43  433  imp5g  447  pm2.61da3ne  3044  onmindif  6460  oaordex  8574  pssnn  9192  alephval3  10196  dfac5  10214  dfac2b  10216  coftr  10358  zorn2lem6  10586  addcanpi  10991  mulcanpi  10992  ltmpi  10996  ltexprlem6  11133  axpre-sup  11261  bndndx  12612  dmdprdd  20224  lssssr  21238  coe1fzgsumdlem  22630  evl1gsumdlem  22683  1stcrest  23780  upgrreslem  29894  umgrreslem  29895  mdsymlem3  33016  mdsymlem6  33019  sumdmdlem  33029  mclsax  36452  mclsppslem  36466  disjlem17  39971  prtlem17  40070  cvratlem  40615  paddidm  41035  pmodlem2  41041  pclfinclN  41144  onexoegt  44383  icceuelpart  48654