Theorem jctild 662

Description: Deduction conjoining a theorem to left of consequent in an implication.

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

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  dfsb2 1595  2eu1 1853  ordunidif 3712  dfwe2 3861  dfwe2OLD 3862  orduniorsuc 3909  xpcan 4348  xpcan2 4350  isofrlem 4878  oeordi 5262  nneob 5312  ssenen 5598  inf3lem3 5721  cfsuc 6063  add20i 6782  nominpos 7230  rpneg 7252  infmrcl 7278  zaddcl 7374  zmulcl 7389  dfuzi 7414  qnegcl 7450  qbtwnre 7459  fsequb 7702  seq1bndi 8162  cvg1 8173  cvg3i 8175  cvganz 8176  caubndi 8178  climshfti 8364  iserzcmp0 8403  caucvglem2 8418  caucvglem4 8420  caucvglem5 8421  infcvglem3 8484  explecnv 8495  cvgratlem4 8515  neiint 8995  metcnpi3 9170  metcnpi4 9171  metcni2 9173  lmnn 9213  lmle 9238  xplmi 9251  xplm 9253  lnon0 9798  ubthlem5 9876  efifolem5 10080  on1el3 10412  spansncol 11124  osumlem4 11216  idcnop 11542  riesz1 11635  hstles 11803  mdsl1i 11893  atcveq0 11920  atcvat4i 11969  cdjreui 12004  tfisg 13912  frmin 13938  poxp 13949  alexsub 15441  reconnlem4 15449  locfincomp 15514  ist1-2 15542  filssufillem 15570  ufcondr 15581  incsequz 15815  mettrifi 15847  txsubsp 15912  sstotbnd 15936  ismtyhmeolem 15950  rrntotbnd 16022  cvrat4 17076  linepsub 17232  pmapsub 17250  osumcllem4 17367  pexmidlem1 17378

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-an 242

Copyright terms: Public domain