Theorem jctil 316

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

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  nic-ax 1239  nic-axALT 1240  unidif 3210  iunxdif2 3301  exss 3516  frirr 3634  limom 3967  dmcosseqOLD 4215  relssres 4248  funcoOLD 4458  fconstOLD 4603  nfunsn 4706  nfunsnOLD 4707  exfo 4795  f1oweALT 4883  fo1stres 5036  fo2ndres 5037  curry2 5078  tfrlem10 5128  odi 5258  undom 5497  sbthlem2 5511  sbthlem3 5512  fodomr 5547  phplem2 5603  pssnn 5628  ordtypelem6 5689  inf3lem6 5724  elomsubsd 5885  kmlem1 5927  brdom5 5964  brdom4 5965  alephval2 6050  cflim 6057  cfsuc 6063  reclem2pr 6309  suplem2pr 6314  supsrlem2 6378  lemulge11 7030  posexi 7091  nnaddm1cl 7142  nnrecl 7281  flhalf 7487  cardfz 7719  seq1f 7736  seq1f2 7737  ser1f 7741  exprecOLD 7838  discrlem3 7908  sqrlem17 7939  abs1mi 8156  seq1ublem 8163  cvgcmp2clemOLD 8443  cvgratlem2ALT 8510  cvgratlem5 8516  efseq0ex 8573  efaddlem10 8609  efaddlem17 8616  ef01tllem1 8645  efgt0i 8669  demoivre 8752  acdc3lem 8754  acdc2lem2 8758  acdc5lem2 8761  acdclem 8763  topcld 8951  ntrss 8964  idcn 9042  opnm 9137  tgioolem 9192  bcthlem18 9294  bcthlem30 9306  grprlidrid 9337  nvge0 9634  sqcn 9674  sspg 9726  ssps 9728  sspmlem 9730  blocnilem 9804  blocni 9805  minveclem31 9920  cdrci 10182  clicls 10183  clint3 10184  filintf 10274  fgfil 10290  hiidge0 10597  bcsiALT 10679  hlim0 10738  hlimcauii 10739  ocsh 10789  occllem6 10811  projlem2 10820  projlem12 10830  projlem13 10831  projlem28 10846  pjthlem10 10861  pjthlem12 10863  ococin 10930  hsupval2 10933  spancl 10937  hsupcl 10940  chabs2 11073  pjoml6i 11165  osumi 11221  osumcor2i 11225  pjss2i 11260  pjssmii 11261  cnlnadjlem7 11643  nmopadjlem 11659  opsqrlem6 11716  stlei 11812  mdslmd1lem1 11897  mdslmd2i 11902  atcvat3i 11968  atcvat4i 11969  sumdmdlem2 11991  dmdbr5ati 11994  bnj545 13271  bnj548 13274  divalglem0 13696  wfr3g 13956  frr3g 13980  axdense 14027  axfelem0 14030  axfelem9 14039  uninqs 14340  domfldrefc 14361  ranfldrefc 14362  domintrefb 14367  repfuntw 14502  prl2 14514  toplat 14638  isppm 14715  curgrpact 14735  topindis 14859  islp3 14861  prtoptop 14919  fgsb 14921  fgsb2 14925  cnfilca 14927  rcfpfil 14934  cntrsetlem 14999  iintlem1 15010  trnij 15015  cnvtr 15016  lvsovso 15038  idfisf 15189  idsubfun 15206  infemb 15207  empistar 15219  cartarlim 15282  trer 15361  fictb 15371  ordtypelem6OLD 15380  elomsubsdOLD 15394  opncldf1 15402  cnsubsp2 15427  hscptsscld 15434  alexsublem4 15440  reconnlem4 15449  isfne3 15482  fnessref 15503  refssfne 15504  comppfsc 15517  neibastop1 15518  neibastop2 15523  neibastop3 15524  topjoin 15527  fnemeet1 15528  fnemeet2 15529  supfil 15560  ufinffr 15578  ufilen 15579  fmfnfm 15598  filnetlem1 15640  filnetlem4 15643  sdclem1 15809  geomcau 15849  heiborlem14 15968  heiborlem33 15987  heiborlem35 15989  phtpyid 16049  phtpycom 16050  phtpycolem5 16055  pcocn 16076  pcohtpylem3 16082  pcorevlem 16086  pcorev 16087  pi1gp 16095  pmapsub 17250

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 164  df-an 242

Copyright terms: Public domain