Theorem imp4a 615

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

Syntax hints:   → wi 4   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  imp4bOLD  617  imp4d  619  imp55  628  imp511  629  reuss2  4050  wefrc  5260  f1oweALT  7318  tfrlem9  7651  tz7.49  7710  oaordex  7809  dfac2b  9163  dfac2OLD  9165  zorn2lem4  9533  zorn2lem7  9536  psslinpr  10065  facwordi  13290  ndvdssub  15355  pmtrfrn  18098  elcls  21099  elcls3  21109  neibl  22527  met2ndc  22549  itgcn  23828  branmfn  29294  atcvatlem  29574  atcvat4i  29586  prtlem15  34682  cvlsupr4  35153  cvlsupr5  35154  cvlsupr6  35155  2llnneN  35216  cvrat4  35250  llnexchb2  35676  cdleme48gfv1  36344  cdlemg6e  36430  dihord6apre  37065  dihord5b  37068  dihord5apre  37071  dihglblem5apreN  37100  dihglbcpreN  37109