Theorem imp4a 428

Description: An importation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Jul-2021.)

Hypothesis

Ref	Expression
imp4.1	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Assertion

Ref	Expression
imp4a	⊢ (𝜑 → (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏)))

Proof of Theorem imp4a

Step	Hyp	Ref	Expression
1		imp4.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
2	1	imp4b 427	. 2 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏))
3	2	ex 418	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:  imp4d  430  imp55  448  imp511  449  reuss2  4271  wefrc  5644  f1oweALT  7985  tfrlem9  8397  tz7.49  8459  oaordex  8570  dfac2b  10213  zorn2lem4  10581  zorn2lem7  10584  psslinpr  11120  facwordi  14437  ndvdssub  16585  pmtrfrn  19678  elcls  23397  elcls3  23407  neibl  24826  met2ndc  24848  itgcn  26171  umgr2cycllem  30752  branmfn  32713  atcvatlem  32993  atcvat4i  33005  satfv0fun  36223  prtlem15  40026  cvlsupr4  40496  cvlsupr5  40497  cvlsupr6  40498  2llnneN  40560  cvrat4  40594  llnexchb2  41020  cdleme48gfv1  41687  cdlemg6e  41773  dihord6apre  42407  dihord5b  42410  dihord5apre  42413  dihglblem5apreN  42442  dihglbcpreN  42451