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

This theorem is referenced by:  imp4d  424  imp55  442  imp511  443  reuss2  4285  wefrc  5625  f1oweALT  7930  tfrlem9  8330  tz7.49  8390  oaordex  8499  dfac2b  10060  zorn2lem4  10428  zorn2lem7  10431  psslinpr  10960  facwordi  14230  ndvdssub  16355  pmtrfrn  19364  elcls  22936  elcls3  22946  neibl  24365  met2ndc  24387  itgcn  25722  branmfn  32007  atcvatlem  32287  atcvat4i  32299  umgr2cycllem  35100  satfv0fun  35331  prtlem15  38841  cvlsupr4  39311  cvlsupr5  39312  cvlsupr6  39313  2llnneN  39376  cvrat4  39410  llnexchb2  39836  cdleme48gfv1  40503  cdlemg6e  40589  dihord6apre  41223  dihord5b  41226  dihord5apre  41229  dihglblem5apreN  41258  dihglbcpreN  41267