Theorem jctil 292

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

Hypotheses

Ref	Expression
jctil.1	|- (ph -> ps)
jctil.2	|- ch

Assertion

Ref	Expression
jctil	|- (ph -> (ch /\ ps))

Proof of Theorem jctil

Step	Hyp	Ref	Expression
1		jctil.2	. . 3 |- ch
2	1	a1i 8	. 2 |- (ph -> ch)
3		jctil.1	. 2 |- (ph -> ps)
4	2, 3	jca 288	1 |- (ph -> (ch /\ ps))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  nicodraw 950  unidif 2525  iunxdif2 2593  exss 2764  frirr 2919  unon 3083  onuninsuc 3103  limom 3141  dmcosseq 3357  relssres 3384  funco 3542  funssres 3544  fconst 3649  ssimaex 3759  exfo 3813  fopabco 3823  fopabcos 3824  fconst2g 3836  f1oweALT 3897  tfrlem10 3911  2ndconst 4087  curry1 4088  oawordeulem 4178  odi 4200  undom 4424  sbthlem2 4434  sbthlem3 4435  sbthlem8 4440  fodomr 4469  phplem2 4495  pssnn 4519  inf3lem6 4598  kmlem1 4745  brdom3 4781  brdom5 4782  brdom4 4783  alephval2 4882  cflim 4889  cfsuc 4895  reclem2pr 5137  suplem2pr 5142  supsrlem2 5206  lemulge11t 5812  posex 5864  nnge1t 5899  nnsub 5911  nnaddm1clt 5913  nnreclt 6027  xrsupsslem 6031  xrinfmsslem 6032  flhalft 6197  seq1f 6268  seq1f2 6269  ser1ft 6273  fznn0t 6456  seqzeq 6495  recexpt 6534  discrlem3 6596  sqrlem17 6627  cj11t 6773  abs1m 6849  seq1ublem 6856  seq1ub 6857  climsup 7099  ser1clim0 7117  cvgcmp2clem 7126  isumclimtf 7139  fnsmnt 7169  georeclim 7183  cvgratlem5 7197  efcltlem1 7254  efseq0ex 7261  efaddlem10 7297  efaddlem17 7304  ef1tllem 7331  ef01tllem1 7333  efgt0 7353  demoivre 7434  acdc3lem 7436  acdc2lem2 7439  acdc5lem2 7442  acdclem 7444  unbenlem 7455  infpnlem2 7458  infdif 7519  tgval3t 7575  topcld 7625  ntrss 7638  idcn 7716  opnm 7812  tgioolem 7866  bcthlem18 7966  bcthlem30 7978  invfval 8213  nvge0 8254  sqcn 8283  sspg 8334  ssps 8336  sspmlem 8338  sspn 8342  nmlno0lem 8398  blocnilem 8408  blocni 8409  minveclem31 8519  hiidge0t 8903  bcsALT 8985  hlim0 9044  hlimcaui 9045  ocsh 9095  occllem6 9117  projlem2 9126  projlem12 9136  projlem13 9137  projlem28 9152  pjthlem10 9166  pjthlem12 9168  ococint 9235  hsupval2t 9238  spanclt 9242  hsupclt 9245  chabs2t 9378  pjoml6 9472  osum 9526  osumcor2 9530  pjss2 9565  pjssm 9566  kbpjt 9819  nmlnop0ALT 9858  cnlnadjlem7 9944  nmopadjlem 9960  pjssdif2 10040  stle 10105  mdslmd1lem1 10189  mdslmd2 10194  atcvat3 10260  atcvat4 10261  sumdmdlem2 10282  dmdbr5at 10284  uninqs 10378  cdrci 10417  filintf 10479  fgsb 10480  fgsb2 10485  cnfilca 10487  clicls 10502  iintlem1 10512  trnij 10517  cnvtr 10518

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