Theorem imp4a 421

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

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  imp4d  423  imp55  441  imp511  442  reuss2  4316  wefrc  5671  f1oweALT  7963  tfrlem9  8389  tz7.49  8449  oaordex  8562  dfac2b  10129  zorn2lem4  10498  zorn2lem7  10501  psslinpr  11030  facwordi  14255  ndvdssub  16358  pmtrfrn  19369  elcls  22799  elcls3  22809  neibl  24232  met2ndc  24254  itgcn  25596  branmfn  31623  atcvatlem  31903  atcvat4i  31915  umgr2cycllem  34427  satfv0fun  34658  prtlem15  38050  cvlsupr4  38520  cvlsupr5  38521  cvlsupr6  38522  2llnneN  38585  cvrat4  38619  llnexchb2  39045  cdleme48gfv1  39712  cdlemg6e  39798  dihord6apre  40432  dihord5b  40435  dihord5apre  40438  dihglblem5apreN  40467  dihglbcpreN  40476