Theorem jctild 600

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

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  dfsb2 1223  2eu1 1447  dfwe2 2930  ordunidif 3000  orduniorsuc 3082  isofrlem 3892  oeordi 4204  nneob 4245  ssenen 4490  inf3lem3 4595  cfsuc 4895  add20 5584  nominpos 5998  infmrcl 6024  zaddclt 6120  zmulclt 6135  dfuz 6158  qnegclt 6216  qbtwnre 6224  fsequb 6463  seq1bnd 6855  cvg1 6866  cvg3 6868  cvganz 6869  caubnd 6871  climshft 7049  iserzcmp0 7087  caucvglem2 7102  caucvglem4 7104  caucvglem5 7105  infcvglem3 7166  cvgratlem4 7196  neiint 7669  metcnpi3 7844  metcnpi4 7845  metcni2 7847  lmnn 7887  lmle 7911  xplmi 7923  xplm 7925  ubthlem5 8477  efifolem5 8660  spansncol 9430  osumlem4 9521  idcnop 9844  riesz1t 9936  hstlest 10096  mdsl1 10185  atcveq0 10212  atcvat4 10261  cdjreu 10293

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 147  df-an 225

Copyright terms: Public domain