Theorem imp4a 614

Description: An importation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Jul-2021.)

Hypothesis

Ref	Expression
imp4.1	|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )

Assertion

Ref	Expression
imp4a	|- ( ph -> ( ps -> ( ( ch /\ th ) -> ta ) ) )

Proof of Theorem imp4a

Step	Hyp	Ref	Expression
1		imp4.1	. . 3 |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
2	1	imp4b 613	. 2 |- ( ( ph /\ ps ) -> ( ( ch /\ th ) -> ta ) )
3	2	ex 450	1 |- ( ph -> ( ps -> ( ( ch /\ th ) -> ta ) ) )

Syntax hints:   -> wi 4   /\ wa 384

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 386

This theorem is referenced by:  imp4bOLD  616  imp4d  618  imp55  627  imp511  628  reuss2  3907  wefrc  5108  f1oweALT  7152  tfrlem9  7481  tz7.49  7540  oaordex  7638  dfac2  8953  zorn2lem4  9321  zorn2lem7  9324  psslinpr  9853  facwordi  13076  ndvdssub  15133  pmtrfrn  17878  elcls  20877  elcls3  20887  neibl  22306  met2ndc  22328  itgcn  23609  branmfn  28964  atcvatlem  29244  atcvat4i  29256  prtlem15  34160  cvlsupr4  34632  cvlsupr5  34633  cvlsupr6  34634  2llnneN  34695  cvrat4  34729  llnexchb2  35155  cdleme48gfv1  35824  cdlemg6e  35910  dihord6apre  36545  dihord5b  36548  dihord5apre  36551  dihglblem5apreN  36580  dihglbcpreN  36589