Theorem jctild 550

Description: Deduction conjoining a theorem to left of consequent in an implication. (Contributed by NM, 21-Apr-2005.)

Hypotheses

Ref	Expression
jctild.1	|- ( ph -> ( ps -> ch ) )
jctild.2	|- ( ph -> th )

Assertion

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

Proof of Theorem jctild

Step	Hyp	Ref	Expression
1		jctild.2	. . 3 |- ( ph -> th )
2	1	a1d 26	. 2 |- ( ph -> ( ps -> th ) )
3		jctild.1	. 2 |- ( ph -> ( ps -> ch ) )
4	2, 3	jcad 540	1 |- ( ph -> ( ps -> ( th /\ ch ) ) )

Syntax hints:   -> wi 4   /\ wa 375

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 190  df-an 377

This theorem is referenced by:  syl6an  552  anc2li  564  ordunidif  5489  isofrlem  6255  dfwe2  6634  orduniorsuc  6683  poxp  6934  fnse  6939  ssenen  7771  dffi3  7970  fpwwe2lem13  9092  zmulcl  11013  rpneg  11360  rexuz3  13459  cau3lem  13465  climrlim2  13659  o1rlimmul  13730  iseralt  13799  gcdeq  14568  isprm3  14681  vdwnnlem2  14994  ablfaclem3  17768  epttop  20072  lmcnp  20368  dfcon2  20482  txcnp  20683  cmphaushmeo  20863  isfild  20921  cnpflf2  21063  flimfnfcls  21091  alexsubALT  21114  fgcfil  22289  bcthlem5  22344  ivthlem2  22451  ivthlem3  22452  dvfsumrlim  23031  plypf1  23214  axeuclidlem  25040  wwlknredwwlkn0  25503  wwlkextwrd  25504  wwlkextproplem1  25517  clwlkisclwwlklem2a1  25555  rusgranumwlklem1  25725  numclwwlkovf2ex  25862  extwwlkfab  25866  lnon0  26487  hstles  27932  mdsl1i  28022  atcveq0  28049  atcvat4i  28098  cdjreui  28133  issgon  28993  conpcon  30006  tfisg  30505  frmin  30528  outsideofrflx  30942  isbasisrelowllem1  31802  isbasisrelowllem2  31803  poimirlem3  31987  poimirlem29  32013  poimir  32017  heicant  32019  equivtotbnd  32154  ismtybndlem  32182  cvrat4  33052  linepsubN  33361  pmapsub  33377  osumcllem4N  33568  pexmidlem1N  33579  dochexmidlem1  35072  clcnvlem  36274  2reu1  38644  iccpartimp  38768  gcdzeq  38830  bgoldbwt  38915  bgoldbst  38916  usgr2wlkneq  39787