Theorem imp4b 613

Description: An importation inference. (Contributed by NM, 26-Apr-1994.) Shorten imp4a 614. (Revised by Wolf Lammen, 19-Jul-2021.)

Hypothesis

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

Assertion

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

Proof of Theorem imp4b

Step	Hyp	Ref	Expression
1		imp4.1	. . 3 |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
2	1	imp 445	. 2 |- ( ( ph /\ ps ) -> ( ch -> ( th -> ta ) ) )
3	2	impd 447	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:  imp4a  614  imp43  621  pm2.61da3ne  2883  onmindif  5815  oaordex  7638  pssnn  8178  alephval3  8933  dfac5  8951  dfac2  8953  coftr  9095  zorn2lem6  9323  addcanpi  9721  mulcanpi  9722  ltmpi  9726  ltexprlem6  9863  axpre-sup  9990  bndndx  11291  relexpaddd  13794  dmdprdd  18398  lssssr  18953  coe1fzgsumdlem  19671  evl1gsumdlem  19720  1stcrest  21256  upgrreslem  26196  umgrreslem  26197  mdsymlem3  29264  mdsymlem6  29267  sumdmdlem  29277  mclsax  31466  mclsppslem  31480  prtlem17  34161  cvratlem  34707  paddidm  35127  pmodlem2  35133  pclfinclN  35236  icceuelpart  41372