Theorem jctild 545

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 535	1 |- ( ph -> ( ps -> ( th /\ ch ) ) )

Syntax hints:   -> wi 4   /\ wa 370

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 188  df-an 372

This theorem is referenced by:  syl6an  547  anc2li  559  ordunidif  5490  isofrlem  6247  dfwe2  6623  orduniorsuc  6672  poxp  6920  fnse  6925  ssenen  7756  dffi3  7955  fpwwe2lem13  9075  zmulcl  10993  rpneg  11340  rexuz3  13412  cau3lem  13418  climrlim2  13611  o1rlimmul  13682  iseralt  13751  gcdeq  14520  isprm3  14633  vdwnnlem2  14946  ablfaclem3  17720  epttop  20023  lmcnp  20319  dfcon2  20433  txcnp  20634  cmphaushmeo  20814  isfild  20872  cnpflf2  21014  flimfnfcls  21042  alexsubALT  21065  fgcfil  22240  bcthlem5  22295  ivthlem2  22402  ivthlem3  22403  dvfsumrlim  22982  plypf1  23165  axeuclidlem  24991  wwlknredwwlkn0  25454  wwlkextwrd  25455  wwlkextproplem1  25468  clwlkisclwwlklem2a1  25506  rusgranumwlklem1  25676  numclwwlkovf2ex  25813  extwwlkfab  25817  lnon0  26438  hstles  27883  mdsl1i  27973  atcveq0  28000  atcvat4i  28049  cdjreui  28084  issgon  28954  conpcon  29967  tfisg  30465  frmin  30488  outsideofrflx  30900  isbasisrelowllem1  31723  isbasisrelowllem2  31724  poimirlem3  31908  poimirlem29  31934  poimir  31938  heicant  31940  equivtotbnd  32075  ismtybndlem  32103  cvrat4  32978  linepsubN  33287  pmapsub  33303  osumcllem4N  33494  pexmidlem1N  33505  dochexmidlem1  34998  clcnvlem  36201  2reu1  38479  iccpartimp  38602  gcdzeq  38664  bgoldbwt  38749  bgoldbst  38750