Theorem jctir 516

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

Hypotheses

Ref	Expression
jctil.1	⊢ (𝜑 → 𝜓)
jctil.2	⊢ 𝜒

Assertion

Ref	Expression
jctir	⊢ (𝜑 → (𝜓 ∧ 𝜒))

Proof of Theorem jctir

Step	Hyp	Ref	Expression
1		jctil.1	. 2 ⊢ (𝜑 → 𝜓)
2		jctil.2	. . 3 ⊢ 𝜒
3	2	a1i 11	. 2 ⊢ (𝜑 → 𝜒)
4	1, 3	jca 507	1 ⊢ (𝜑 → (𝜓 ∧ 𝜒))

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 198  df-an 385

This theorem is referenced by:  jctr  520  uniintsn  4670  ordunidif  5956  funtp  6124  foimacnv  6337  respreima  6534  fpr  6613  curry1  7471  dmtpos  7567  wfrlem13  7631  oawordeulem  7839  oelim2  7880  oaabs2  7930  ixpsnf1o  8153  ssdomg  8206  fodomr  8318  limenpsi  8342  cantnfrescl  8788  cardprclem  9056  fin4en1  9384  ssfin4  9385  axdc3lem2  9526  axdc3lem4  9528  fpwwe2lem9  9713  reclem2pr  10123  recexsrlem  10177  nn0n0n1ge2b  11606  xmulpnf1  12306  ige2m2fzo  12739  swrdlsw  13654  swrd2lsw  13983  wrdl3s3  13994  climeu  14573  algcvgblem  15573  lcmfass  15642  qredeu  15654  qnumdencoprm  15734  qeqnumdivden  15735  isacs1i  16585  subgga  17998  symgfixf1  18122  sylow1lem2  18280  sylow3lem1  18308  nn0gsumfz  18646  mptcoe1fsupp  19858  evls1gsumadd  19962  evls1gsummul  19963  evl1gsummul  19997  mat1scmat  20622  smadiadetlem4  20753  mptcoe1matfsupp  20886  chfacfscmulgsum  20944  chfacfpmmulgsum  20948  eltg3i  21045  topbas  21056  neips  21197  lmbrf  21344  rnelfm  22036  tsmsres  22226  reconnlem1  22908  lmmbrf  23339  iscauf  23357  caucfil  23360  cmetcaulem  23365  voliunlem1  23608  isosctrlem1  24839  bcmono  25293  2lgslem1a  25407  dchrvmasumlem2  25478  mulog2sumlem2  25515  pntlemb  25577  axlowdimlem13  26125  usgr2pthlem  26950  2pthon3v  27146  elwspths2spth  27172  clwwlkccatlem  27195  clwlkclwwlklem2fv2  27202  clwlksf1clwwlkOLD  27306  grpofo  27745  nvss  27839  nmosetn0  28011  hhsst  28514  pjoc1i  28681  chlejb1i  28726  cmbr4i  28851  pjjsi  28950  nmopun  29264  stlesi  29491  mdsl2bi  29573  mdslmd1lem1  29575  xraddge02  29905  supxrnemnf  29918  qtopt1  30284  lmxrge0  30380  esumcst  30507  sigagenval  30585  measdivcstOLD  30669  oms0  30741  ballotlemfc0  30937  ballotlemfcc  30938  bnj945  31224  bnj150  31326  bnj986  31404  bnj1421  31490  fv1stcnv  32055  fv2ndcnv  32056  dftrpred3g  32108  nodense  32218  nulssgt  32285  conway  32286  etasslt  32296  slerec  32299  fness  32719  nandsym1  32792  bj-finsumval0  33513  finixpnum  33750  poimirlem3  33768  poimirlem16  33781  poimirlem17  33782  poimirlem19  33784  poimirlem20  33785  poimirlem27  33792  ismblfin  33806  lcvexchlem5  34926  paddssat  35702  dibn0  37041  lclkrs2  37428  fiphp3d  37993  pellqrex  38053  jm2.16nn0  38180  rp-fakeanorass  38466  clsk1indlem2  38946  icccncfext  40670  wallispilem4  40854  fmtnorec1  42057  fmtnoprmfac1lem  42084  mod42tp1mod8  42127  stgoldbwt  42272  sbgoldbwt  42273  sbgoldbst  42274  evengpoap3  42295  wtgoldbnnsum4prm  42298  bgoldbnnsum3prm  42300  ply1mulgsumlem2  42776  ldepspr  42863  blennngt2o2  42987