Theorem jctir 561

Description: Inference conjoining a theorem to right of consequent in an implication. (Contributed by NM, 31-Dec-1993.)

Hypotheses

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

Assertion

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

Proof of Theorem jctir

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

Syntax hints:   -> wi 4   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  jctr  565  uniintsn  4514  ordunidif  5773  funtp  5945  foimacnv  6154  respreima  6344  fpr  6421  curry1  7269  dmtpos  7364  wfrlem13  7427  oawordeulem  7634  oelim2  7675  oaabs2  7725  ixpsnf1o  7948  ssdomg  8001  fodomr  8111  limenpsi  8135  cantnfrescl  8573  cardprclem  8805  fin4en1  9131  ssfin4  9132  axdc3lem2  9273  axdc3lem4  9275  fpwwe2lem9  9460  reclem2pr  9870  recexsrlem  9924  nn0n0n1ge2b  11359  xmulpnf1  12104  ige2m2fzo  12530  swrdlsw  13452  swrd2lsw  13695  wrdl3s3  13705  climeu  14286  algcvgblem  15290  lcmfass  15359  qredeu  15372  qnumdencoprm  15453  qeqnumdivden  15454  isacs1i  16318  subgga  17733  symgfixf1  17857  sylow1lem2  18014  sylow3lem1  18042  nn0gsumfz  18380  mptcoe1fsupp  19585  evls1gsumadd  19689  evls1gsummul  19690  evl1gsummul  19724  mat1scmat  20345  smadiadetlem4  20475  mptcoe1matfsupp  20607  chfacfscmulgsum  20665  chfacfpmmulgsum  20669  eltg3i  20765  topbas  20776  neips  20917  lmbrf  21064  rnelfm  21757  tsmsres  21947  reconnlem1  22629  lmmbrf  23060  iscauf  23078  caucfil  23081  cmetcaulem  23086  voliunlem1  23318  isosctrlem1  24548  bcmono  25002  2lgslem1a  25116  dchrvmasumlem2  25187  mulog2sumlem2  25224  pntlemb  25286  axlowdimlem13  25834  usgr2pthlem  26659  2pthon3v  26839  elwspths2spth  26862  clwlkclwwlklem2fv2  26897  clwlksf1clwwlk  26969  grpofo  27353  nvss  27448  nmosetn0  27620  hhsst  28123  pjoc1i  28290  chlejb1i  28335  cmbr4i  28460  pjjsi  28559  nmopun  28873  stlesi  29100  mdsl2bi  29182  mdslmd1lem1  29184  xraddge02  29521  supxrnemnf  29534  qtopt1  29902  lmxrge0  29998  esumcst  30125  sigagenval  30203  measdivcstOLD  30287  oms0  30359  ballotlemfc0  30554  ballotlemfcc  30555  bnj945  30844  bnj150  30946  bnj986  31024  bnj1421  31110  dftrpred3g  31733  nodense  31842  nulssgt  31909  conway  31910  etasslt  31920  slerec  31923  fness  32344  nandsym1  32421  bj-finsumval0  33147  finixpnum  33394  poimirlem3  33412  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem27  33436  ismblfin  33450  rngoideu  33702  lcvexchlem5  34325  paddssat  35100  dibn0  36442  lclkrs2  36829  fiphp3d  37383  pellqrex  37443  jm2.16nn0  37571  rp-fakeanorass  37858  clsk1indlem2  38340  icccncfext  40100  wallispilem4  40285  fmtnorec1  41449  fmtnoprmfac1lem  41476  mod42tp1mod8  41519  stgoldbwt  41664  sbgoldbwt  41665  sbgoldbst  41666  evengpoap3  41687  wtgoldbnnsum4prm  41690  bgoldbnnsum3prm  41692  ply1mulgsumlem2  42175  ldepspr  42262  blennngt2o2  42386