Theorem jctir 520

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 511	1 ⊢ (𝜑 → (𝜓 ∧ 𝜒))

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  jctr  524  ordunidif  6370  funtp  6557  dmtpos  8194  frrlem11  8252  oaabs2  8590  ixpsnf1o  8888  fodomr  9069  fodomfir  9255  mapfienlem2  9333  cantnfrescl  9605  dfttrcl2  9653  cardprclem  9908  fin4en1  10238  ssfin4  10239  axdc3lem2  10380  axdc3lem4  10382  fpwwe2lem8  10567  recexsrlem  11032  nn0n0n1ge2b  12487  xmulpnf1  13210  ige2m2fzo  13665  swrdlsw  14608  swrd2lsw  14894  wrdl3s3  14904  lcmfass  16592  qredeu  16604  qnumdencoprm  16691  qeqnumdivden  16692  isacs1i  17598  subgga  19214  symgfixf1  19351  sylow1lem2  19513  sylow3lem1  19541  nn0gsumfz  19898  pzriprngALT  21437  evlsgsumadd  22031  evlsgsummul  22032  mhpmulcl  22069  mptcoe1fsupp  22133  evls1gsumadd  22244  evls1gsummul  22245  evl1gsummul  22280  mat1scmat  22459  smadiadetlem4  22589  mptcoe1matfsupp  22722  chfacfscmulgsum  22780  chfacfpmmulgsum  22784  topbas  22892  neips  23033  lmbrf  23180  rnelfm  23873  tsmsres  24064  reconnlem1  24748  lmmbrf  25195  iscauf  25213  caucfil  25216  cmetcaulem  25221  voliunlem1  25484  isosctrlem1  26761  bcmono  27221  2lgslem1a  27335  dchrvmasumlem2  27442  mulog2sumlem2  27479  pntlemb  27541  nodense  27637  conway  27745  etasslt  27759  slerec  27765  cofcutr  27872  precsexlem9  28157  usgr2pthlem  29743  2pthon3v  29923  elwspths2spth  29947  clwlkclwwlklem2fv2  29975  grpofo  30478  nvss  30572  nmosetn0  30744  hhsst  31245  pjoc1i  31410  chlejb1i  31455  cmbr4i  31580  pjjsi  31679  nmopun  31993  stlesi  32220  mdsl2bi  32302  mdslmd1lem1  32304  xraddge02  32730  supxrnemnf  32741  constrextdg2  33732  qtopt1  33818  lmxrge0  33935  esumcst  34046  sigagenval  34123  measdivcstALTV  34208  oms0  34281  ballotlemfc0  34477  ballotlemfcc  34478  bnj945  34756  bnj986  34938  bnj1421  35025  fv1stcnv  35757  fv2ndcnv  35758  fness  36330  nandsym1  36403  bj-finsumval0  37266  finixpnum  37592  poimirlem3  37610  poimirlem16  37623  poimirlem17  37624  poimirlem19  37626  poimirlem20  37627  poimirlem27  37634  ismblfin  37648  lcvexchlem5  39024  paddssat  39801  dibn0  41140  lclkrs2  41527  aks4d1p1p7  42055  eqresfnbd  42213  fiphp3d  42800  pellqrex  42860  jm2.16nn0  42986  onexlimgt  43225  cantnf2  43307  rp-fakeanorass  43495  clsk1indlem2  44024  icccncfext  45878  wallispilem4  46059  fmtnorec1  47531  fmtnoprmfac1lem  47558  mod42tp1mod8  47596  stgoldbwt  47770  sbgoldbwt  47771  sbgoldbst  47772  evengpoap3  47793  wtgoldbnnsum4prm  47796  bgoldbnnsum3prm  47798  isubgruhgr  47861  uhgrimisgrgric  47924  isubgr3stgrlem7  47964  gpgprismgr4cycl0  48089  ply1mulgsumlem2  48369  ldepspr  48455  blennngt2o2  48574  inlinecirc02plem  48768