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  6385  funtp  6576  dmtpos  8220  frrlem11  8278  oaabs2  8616  ixpsnf1o  8914  fodomr  9098  fodomfir  9286  mapfienlem2  9364  cantnfrescl  9636  dfttrcl2  9684  cardprclem  9939  fin4en1  10269  ssfin4  10270  axdc3lem2  10411  axdc3lem4  10413  fpwwe2lem8  10598  recexsrlem  11063  nn0n0n1ge2b  12518  xmulpnf1  13241  ige2m2fzo  13696  swrdlsw  14639  swrd2lsw  14925  wrdl3s3  14935  lcmfass  16623  qredeu  16635  qnumdencoprm  16722  qeqnumdivden  16723  isacs1i  17625  subgga  19239  symgfixf1  19374  sylow1lem2  19536  sylow3lem1  19564  nn0gsumfz  19921  pzriprngALT  21412  evlsgsumadd  22005  evlsgsummul  22006  mhpmulcl  22043  mptcoe1fsupp  22107  evls1gsumadd  22218  evls1gsummul  22219  evl1gsummul  22254  mat1scmat  22433  smadiadetlem4  22563  mptcoe1matfsupp  22696  chfacfscmulgsum  22754  chfacfpmmulgsum  22758  topbas  22866  neips  23007  lmbrf  23154  rnelfm  23847  tsmsres  24038  reconnlem1  24722  lmmbrf  25169  iscauf  25187  caucfil  25190  cmetcaulem  25195  voliunlem1  25458  isosctrlem1  26735  bcmono  27195  2lgslem1a  27309  dchrvmasumlem2  27416  mulog2sumlem2  27453  pntlemb  27515  nodense  27611  conway  27718  etasslt  27732  slerec  27738  cofcutr  27839  precsexlem9  28124  usgr2pthlem  29700  2pthon3v  29880  elwspths2spth  29904  clwlkclwwlklem2fv2  29932  grpofo  30435  nvss  30529  nmosetn0  30701  hhsst  31202  pjoc1i  31367  chlejb1i  31412  cmbr4i  31537  pjjsi  31636  nmopun  31950  stlesi  32177  mdsl2bi  32259  mdslmd1lem1  32261  xraddge02  32687  supxrnemnf  32698  constrextdg2  33746  qtopt1  33832  lmxrge0  33949  esumcst  34060  sigagenval  34137  measdivcstALTV  34222  oms0  34295  ballotlemfc0  34491  ballotlemfcc  34492  bnj945  34770  bnj986  34952  bnj1421  35039  fv1stcnv  35771  fv2ndcnv  35772  fness  36344  nandsym1  36417  bj-finsumval0  37280  finixpnum  37606  poimirlem3  37624  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem27  37648  ismblfin  37662  lcvexchlem5  39038  paddssat  39815  dibn0  41154  lclkrs2  41541  aks4d1p1p7  42069  eqresfnbd  42227  fiphp3d  42814  pellqrex  42874  jm2.16nn0  43000  onexlimgt  43239  cantnf2  43321  rp-fakeanorass  43509  clsk1indlem2  44038  icccncfext  45892  wallispilem4  46073  fmtnorec1  47542  fmtnoprmfac1lem  47569  mod42tp1mod8  47607  stgoldbwt  47781  sbgoldbwt  47782  sbgoldbst  47783  evengpoap3  47804  wtgoldbnnsum4prm  47807  bgoldbnnsum3prm  47809  isubgruhgr  47872  uhgrimisgrgric  47935  isubgr3stgrlem7  47975  gpgprismgr4cycl0  48100  ply1mulgsumlem2  48380  ldepspr  48466  blennngt2o2  48585  inlinecirc02plem  48779