Theorem imp4b 422

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  imp4a  423  imp43  428  imp5g  442  pm2.61da3ne  3023  onmindif  6404  oaordex  8483  pssnn  9093  alephval3  10023  dfac5  10042  dfac2b  10044  coftr  10186  zorn2lem6  10414  addcanpi  10813  mulcanpi  10814  ltmpi  10818  ltexprlem6  10955  axpre-sup  11083  bndndx  12427  dmdprdd  19967  lssssr  20944  coe1fzgsumdlem  22289  evl1gsumdlem  22342  1stcrest  23436  upgrreslem  29391  umgrreslem  29392  mdsymlem3  32494  mdsymlem6  32497  sumdmdlem  32507  mclsax  35797  mclsppslem  35811  disjlem17  39269  prtlem17  39368  cvratlem  39913  paddidm  40333  pmodlem2  40339  pclfinclN  40442  onexoegt  43689  icceuelpart  47911