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  4274  wefrc  5652  f1oweALT  8018  tfrlem9  8431  tz7.49  8493  oaordex  8604  dfac2b  10248  zorn2lem4  10616  zorn2lem7  10619  psslinpr  11155  facwordi  14474  ndvdssub  16623  pmtrfrn  19723  elcls  23446  elcls3  23456  neibl  24875  met2ndc  24897  itgcn  26220  umgr2cycllem  30803  branmfn  32764  atcvatlem  33044  atcvat4i  33056  satfv0fun  36344  prtlem15  40198  cvlsupr4  40668  cvlsupr5  40669  cvlsupr6  40670  2llnneN  40732  cvrat4  40766  llnexchb2  41192  cdleme48gfv1  41859  cdlemg6e  41945  dihord6apre  42579  dihord5b  42582  dihord5apre  42585  dihglblem5apreN  42614  dihglbcpreN  42623