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  2363  reusv7OLD  4649  ordunidif  4916  isofrlem  6221  dfwe2  6602  orduniorsuc  6650  poxp  6897  fnse  6902  ssenen  7693  dffi3  7893  fpwwe2lem13  9023  zmulcl  10919  rpneg  11260  rexuz3  13163  cau3lem  13169  climrlim2  13352  o1rlimmul  13423  iseralt  13489  gcdeq  14172  isprm3  14208  vdwnnlem2  14496  ablfaclem3  17117  epttop  19488  lmcnp  19783  dfcon2  19898  txcnp  20099  cmphaushmeo  20279  isfild  20337  cnpflf2  20479  flimfnfcls  20507  alexsubALT  20529  fgcfil  21688  bcthlem5  21745  ivthlem2  21842  ivthlem3  21843  dvfsumrlim  22410  plypf1  22587  axeuclidlem  24243  wwlknredwwlkn0  24705  wwlkextwrd  24706  wwlkextproplem1  24719  clwlkisclwwlklem2a1  24757  rusgranumwlklem1  24927  numclwwlkovf2ex  25064  extwwlkfab  25068  lnon0  25691  hstles  27128  mdsl1i  27218  atcveq0  27245  atcvat4i  27294  cdjreui  27329  issgon  28101  conpcon  28658  tfisg  29260  frmin  29298  outsideofrflx  29753  heicant  30025  equivtotbnd  30250  ismtybndlem  30278  2reu1  32145  bj-iffal  34036  cvrat4  35042  linepsubN  35351  pmapsub  35367  osumcllem4N  35558  pexmidlem1N  35569  dochexmidlem1  37062