Theorem imp4a 422

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 421	. 2 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏))
3	2	ex 412	1 ⊢ (𝜑 → (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏)))

Syntax hints:   → wi 4   ∧ wa 395

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 206  df-an 396

This theorem is referenced by:  imp4d  424  imp55  442  imp511  443  reuss2  4246  wefrc  5574  f1oweALT  7788  tfrlem9  8187  tz7.49  8246  oaordex  8351  dfac2b  9817  zorn2lem4  10186  zorn2lem7  10189  psslinpr  10718  facwordi  13931  ndvdssub  16046  pmtrfrn  18981  elcls  22132  elcls3  22142  neibl  23563  met2ndc  23585  itgcn  24914  branmfn  30368  atcvatlem  30648  atcvat4i  30660  umgr2cycllem  33002  satfv0fun  33233  prtlem15  36816  cvlsupr4  37286  cvlsupr5  37287  cvlsupr6  37288  2llnneN  37350  cvrat4  37384  llnexchb2  37810  cdleme48gfv1  38477  cdlemg6e  38563  dihord6apre  39197  dihord5b  39200  dihord5apre  39203  dihglblem5apreN  39232  dihglbcpreN  39241