Theorem jctild 543

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 25	. 2 |- ( ph -> ( ps -> th ) )
3		jctild.1	. 2 |- ( ph -> ( ps -> ch ) )
4	2, 3	jcad 533	1 |- ( ph -> ( ps -> ( th /\ ch ) ) )

Syntax hints:   -> wi 4   /\ wa 369

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 185  df-an 371

This theorem is referenced by:  syl6an  545  anc2li  557  2eu1OLD  2387  reusv7OLD  4659  ordunidif  4926  isofrlem  6223  dfwe2  6596  orduniorsuc  6644  poxp  6895  fnse  6900  ssenen  7691  dffi3  7890  fpwwe2lem13  9019  zmulcl  10910  rpneg  11248  rexuz3  13143  cau3lem  13149  climrlim2  13332  o1rlimmul  13403  iseralt  13469  gcdeq  14048  isprm3  14084  vdwnnlem2  14372  ablfaclem3  16937  epttop  19292  lmcnp  19587  dfcon2  19702  txcnp  19872  cmphaushmeo  20052  isfild  20110  cnpflf2  20252  flimfnfcls  20280  alexsubALT  20302  fgcfil  21461  bcthlem5  21518  ivthlem2  21615  ivthlem3  21616  dvfsumrlim  22183  plypf1  22360  axeuclidlem  23957  wwlknredwwlkn0  24419  wwlkextwrd  24420  wwlkextproplem1  24433  clwlkisclwwlklem2a1  24471  rusgranumwlklem1  24641  numclwwlkovf2ex  24779  extwwlkfab  24783  lnon0  25405  hstles  26842  mdsl1i  26932  atcveq0  26959  atcvat4i  27008  cdjreui  27043  issgon  27779  conpcon  28336  tfisg  28877  frmin  28915  outsideofrflx  29370  heicant  29642  equivtotbnd  29893  ismtybndlem  29921  2reu1  31674  bj-iffal  33243  cvrat4  34248  linepsubN  34557  pmapsub  34573  osumcllem4N  34764  pexmidlem1N  34775  dochexmidlem1  36266