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  4279  wefrc  5657  f1oweALT  7971  tfrlem9  8374  tz7.49  8434  oaordex  8545  dfac2b  10126  zorn2lem4  10494  zorn2lem7  10497  psslinpr  11027  facwordi  14339  ndvdssub  16485  pmtrfrn  19552  elcls  23260  elcls3  23270  neibl  24689  met2ndc  24711  itgcn  26035  umgr2cycllem  30549  branmfn  32504  atcvatlem  32784  atcvat4i  32796  satfv0fun  35876  prtlem15  39682  cvlsupr4  40152  cvlsupr5  40153  cvlsupr6  40154  2llnneN  40216  cvrat4  40250  llnexchb2  40676  cdleme48gfv1  41343  cdlemg6e  41429  dihord6apre  42063  dihord5b  42066  dihord5apre  42069  dihglblem5apreN  42098  dihglbcpreN  42107