Theorem imp4a 415

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

Syntax hints:   → wi 4   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  imp4d  417  imp55  435  imp511  436  reuss2  4135  wefrc  5335  f1oweALT  7411  tfrlem9  7746  tz7.49  7805  oaordex  7904  dfac2b  9265  dfac2OLD  9267  zorn2lem4  9635  zorn2lem7  9638  psslinpr  10167  facwordi  13368  ndvdssub  15505  pmtrfrn  18227  elcls  21247  elcls3  21257  neibl  22675  met2ndc  22697  itgcn  24007  branmfn  29518  atcvatlem  29798  atcvat4i  29810  prtlem15  34949  cvlsupr4  35419  cvlsupr5  35420  cvlsupr6  35421  2llnneN  35483  cvrat4  35517  llnexchb2  35943  cdleme48gfv1  36610  cdlemg6e  36696  dihord6apre  37330  dihord5b  37333  dihord5apre  37336  dihglblem5apreN  37365  dihglbcpreN  37374