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  2365  reusv7OLD  4504  ordunidif  4767  isofrlem  6031  dfwe2  6393  orduniorsuc  6441  poxp  6684  fnse  6689  ssenen  7485  dffi3  7681  fpwwe2lem13  8809  zmulcl  10693  rpneg  11020  rexuz3  12836  cau3lem  12842  climrlim2  13025  o1rlimmul  13096  iseralt  13162  gcdeq  13736  isprm3  13772  vdwnnlem2  14057  ablfaclem3  16588  epttop  18613  lmcnp  18908  dfcon2  19023  txcnp  19193  cmphaushmeo  19373  isfild  19431  cnpflf2  19573  flimfnfcls  19601  alexsubALT  19623  fgcfil  20782  bcthlem5  20839  ivthlem2  20936  ivthlem3  20937  dvfsumrlim  21503  plypf1  21680  axeuclidlem  23208  lnon0  24198  hstles  25635  mdsl1i  25725  atcveq0  25752  atcvat4i  25801  cdjreui  25836  issgon  26566  conpcon  27124  tfisg  27665  frmin  27703  outsideofrflx  28158  heicant  28426  equivtotbnd  28677  ismtybndlem  28705  2reu1  30010  wwlknredwwlkn0  30359  wwlkextwrd  30360  clwlkisclwwlklem2a1  30441  wwlkextproplem1  30560  rusgranumwlklem1  30567  numclwwlkovf2ex  30679  extwwlkfab  30683  bj-iffal  32090  cvrat4  33087  linepsubN  33396  pmapsub  33412  osumcllem4N  33603  pexmidlem1N  33614  dochexmidlem1  35105