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 954  unidif 2534  iunxdif2 2602  exss 2775  frirr 2930  unon 3094  onuninsuc 3114  limom 3152  dmcosseq 3371  relssres 3398  funco 3556  funssres 3558  fconst 3664  ssimaex 3774  exfo 3828  fopabco 3838  fopabcos 3839  fconst2g 3851  f1oweALT 3912  tfrlem10 3926  2ndconst 4103  curry1 4104  oawordeulem 4194  odi 4216  undom 4444  sbthlem2 4454  sbthlem3 4455  sbthlem8 4460  fodomr 4489  phplem2 4515  pssnn 4544  inf3lem6 4627  kmlem1 4775  brdom3 4811  brdom5 4812  brdom4 4813  alephval2 4913  cflim 4921  cfsuc 4927  reclem2pr 5169  suplem2pr 5174  supsrlem2 5238  lemulge11t 5850  posex 5910  nnge1t 5945  nnsub 5958  nnaddm1clt 5960  nnreclt 6074  xrsupsslem 6078  xrinfmsslem 6079  flhalft 6248  seq1f 6324  seq1f2 6325  ser1ft 6329  fznn0t 6517  seqzeq 6556  recexpt 6596  discrlem3 6659  sqrlem17 6690  cj11t 6830  abs1m 6904  seq1ublem 6911  seq1ub 6912  climsup 7155  ser1clim0 7173  cvgcmp2clem 7182  isumclimtf 7195  fnsmnt 7226  georeclim 7240  cvgratlem5 7254  efcltlem1 7304  efseq0ex 7311  efaddlem10 7347  efaddlem17 7354  ef1tllem 7381  ef01tllem1 7383  efgt0 7404  demoivre 7485  acdc3lem 7487  acdc2lem2 7490  acdc5lem2 7493  acdclem 7495  unbenlem 7505  infpnlem2 7508  infdif 7569  tgval3t 7624  topcld 7672  ntrss 7685  idcn 7763  opnm 7857  tgioolem 7911  bcthlem18 8013  bcthlem30 8025  invfval 8257  nvge0 8298  sqcn 8331  sspg 8383  ssps 8385  sspmlem 8387  sspn 8391  nmlno0lem 8449  blocnilem 8460  blocni 8461  minveclem31 8571  hiidge0t 8959  bcsALT 9041  hlim0 9100  hlimcaui 9101  ocsh 9151  occllem6 9173  projlem2 9182  projlem12 9192  projlem13 9193  projlem28 9208  pjthlem10 9223  pjthlem12 9225  ococint 9292  hsupval2t 9295  spanclt 9299  hsupclt 9302  chabs2t 9435  pjoml6 9527  osum 9581  osumcor2 9585  pjss2 9620  pjssm 9621  kbpjt 9875  nmlnop0ALT 9915  cnlnadjlem7 10001  nmopadjlem 10017  pjssdif2 10097  stle 10162  mdslmd1lem1 10247  mdslmd2 10252  atcvat3 10318  atcvat4 10319  sumdmdlem2 10341  dmdbr5at 10344  uninqs 10436  cdrci 10480  filintf 10554  fgsb 10555  fgsb2 10560  cnfilca 10562  rcfpfil 10569  clicls 10593  iintlem1 10603  trnij 10608  cnvtr 10609  idfisf 10731

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