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  6375  funtp  6557  dmtpos  8190  frrlem11  8248  oaabs2  8587  ixpsnf1o  8888  fodomr  9068  fodomfir  9240  mapfienlem2  9321  cantnfrescl  9597  dfttrcl2  9645  cardprclem  9903  fin4en1  10231  ssfin4  10232  axdc3lem2  10373  axdc3lem4  10375  fpwwe2lem8  10561  recexsrlem  11026  nn0n0n1ge2b  12482  xmulpnf1  13201  ige2m2fzo  13656  swrdlsw  14603  swrd2lsw  14887  wrdl3s3  14897  lcmfass  16585  qredeu  16597  qnumdencoprm  16684  qeqnumdivden  16685  isacs1i  17592  subgga  19241  symgfixf1  19378  sylow1lem2  19540  sylow3lem1  19568  nn0gsumfz  19925  pzriprngALT  21462  evlsgsumadd  22063  evlsgsummul  22064  mhpmulcl  22104  mptcoe1fsupp  22168  evls1gsumadd  22280  evls1gsummul  22281  evl1gsummul  22316  mat1scmat  22495  smadiadetlem4  22625  mptcoe1matfsupp  22758  chfacfscmulgsum  22816  chfacfpmmulgsum  22820  topbas  22928  neips  23069  lmbrf  23216  rnelfm  23909  tsmsres  24100  reconnlem1  24783  lmmbrf  25230  iscauf  25248  caucfil  25251  cmetcaulem  25256  voliunlem1  25519  isosctrlem1  26796  bcmono  27256  2lgslem1a  27370  dchrvmasumlem2  27477  mulog2sumlem2  27514  pntlemb  27576  nodense  27672  conway  27787  etaslts  27801  lesrec  27807  cofcutr  27932  precsexlem9  28223  usgr2pthlem  29848  2pthon3v  30028  elwspths2spth  30055  clwlkclwwlklem2fv2  30083  grpofo  30587  nvss  30681  nmosetn0  30853  hhsst  31354  pjoc1i  31519  chlejb1i  31564  cmbr4i  31689  pjjsi  31788  nmopun  32102  stlesi  32329  mdsl2bi  32411  mdslmd1lem1  32413  xraddge02  32848  supxrnemnf  32859  evlextv  33719  constrextdg2  33927  qtopt1  34013  lmxrge0  34130  esumcst  34241  sigagenval  34318  measdivcstALTV  34403  oms0  34475  ballotlemfc0  34671  ballotlemfcc  34672  bnj945  34950  bnj986  35131  bnj1421  35218  fv1stcnv  35993  fv2ndcnv  35994  fness  36565  nandsym1  36638  bj-finsumval0  37540  finixpnum  37856  poimirlem3  37874  poimirlem16  37887  poimirlem17  37888  poimirlem19  37890  poimirlem20  37891  poimirlem27  37898  ismblfin  37912  ecxrn2  38659  lcvexchlem5  39414  paddssat  40190  dibn0  41529  lclkrs2  41916  aks4d1p1p7  42444  eqresfnbd  42604  fiphp3d  43176  pellqrex  43236  jm2.16nn0  43361  onexlimgt  43600  cantnf2  43682  rp-fakeanorass  43869  clsk1indlem2  44398  icccncfext  46245  wallispilem4  46426  fmtnorec1  47897  fmtnoprmfac1lem  47924  mod42tp1mod8  47962  stgoldbwt  48136  sbgoldbwt  48137  sbgoldbst  48138  evengpoap3  48159  wtgoldbnnsum4prm  48162  bgoldbnnsum3prm  48164  isubgruhgr  48228  uhgrimisgrgric  48291  isubgr3stgrlem7  48332  gpgprismgr4cycl0  48466  ply1mulgsumlem2  48747  ldepspr  48833  blennngt2o2  48952  inlinecirc02plem  49146