Theorem jctild 599

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

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  dfsb2 1220  2eu1 1442  dfwe2 2925  ordunidif 2995  orduniorsuc 3077  isofrlem 3886  oeordi 4198  nneob 4239  ssenen 4484  inf3lem3 4587  cfsuc 4887  add20 5576  nominpos 5990  infmrcl 6016  zaddclt 6112  zmulclt 6127  dfuz 6150  qnegclt 6208  qbtwnre 6216  fsequb 6455  seq1bnd 6847  cvg1 6858  cvg3 6860  cvganz 6861  caubnd 6863  climshft 7041  iserzcmp0 7079  caucvglem2 7094  caucvglem4 7096  caucvglem5 7097  infcvglem3 7158  cvgratlem4 7188  neiint 7660  metcnpi3 7831  metcnpi4 7832  metcni2 7834  lmnn 7873  lmle 7895  xplmi 7907  xplm 7909  ubthlem5 8464  efifolem5 8641  spansncol 9407  osumlem4 9498  idcnop 9821  riesz1t 9913  hstlest 10068  mdsl1 10156  atcveq0 10183  atcvat4 10232  cdjreu 10264

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