Theorem jctild 601

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 600	1 |- (ph -> (ps -> (th /\ ch)))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  dfsb2 1225  2eu1 1449  dfwe2 2935  ordunidif 3005  orduniorsuc 3087  isofrlem 3901  oeordi 4214  nneob 4255  ssenen 4504  inf3lem3 4615  cfsuc 4915  add20 5602  nominpos 6043  infmrcl 6069  zaddclt 6165  zmulclt 6180  dfuz 6202  qnegclt 6270  qbtwnre 6278  fsequb 6523  seq1bnd 6910  cvg1 6921  cvg3 6923  cvganz 6924  caubnd 6926  climshft 7104  iserzcmp0 7143  caucvglem2 7158  caucvglem4 7160  caucvglem5 7161  infcvglem3 7223  cvgratlem4 7253  neiint 7719  metcnpi3 7892  metcnpi4 7893  metcni2 7895  lmnn 7935  lmle 7960  xplmi 7973  xplm 7975  lnon0 8458  ubthlem5 8533  efifolem5 8726  spansncol 9491  osumlem4 9581  idcnop 9905  riesz1t 9998  hstlest 10158  mdsl1 10248  atcveq0 10275  atcvat4 10324  cdjreu 10359

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