Theorem jctir 521

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  jctr  525  ordunidif  6413  funtp  6605  dmtpos  8222  frrlem11  8280  oaabs2  8647  ixpsnf1o  8931  fodomr  9127  mapfienlem2  9400  cantnfrescl  9670  dfttrcl2  9718  cardprclem  9973  fin4en1  10303  ssfin4  10304  axdc3lem2  10445  axdc3lem4  10447  fpwwe2lem8  10632  recexsrlem  11097  nn0n0n1ge2b  12539  xmulpnf1  13252  ige2m2fzo  13694  swrdlsw  14616  swrd2lsw  14902  wrdl3s3  14912  lcmfass  16582  qredeu  16594  qnumdencoprm  16680  qeqnumdivden  16681  isacs1i  17600  subgga  19163  symgfixf1  19304  sylow1lem2  19466  sylow3lem1  19494  nn0gsumfz  19851  evlsgsumadd  21653  evlsgsummul  21654  mhpmulcl  21691  mptcoe1fsupp  21738  evls1gsumadd  21842  evls1gsummul  21843  evl1gsummul  21878  mat1scmat  22040  smadiadetlem4  22170  mptcoe1matfsupp  22303  chfacfscmulgsum  22361  chfacfpmmulgsum  22365  topbas  22474  neips  22616  lmbrf  22763  rnelfm  23456  tsmsres  23647  reconnlem1  24341  lmmbrf  24778  iscauf  24796  caucfil  24799  cmetcaulem  24804  voliunlem1  25066  isosctrlem1  26320  bcmono  26777  2lgslem1a  26891  dchrvmasumlem2  26998  mulog2sumlem2  27035  pntlemb  27097  nodense  27192  conway  27297  etasslt  27311  slerec  27317  cofcutr  27408  precsexlem9  27658  usgr2pthlem  29017  2pthon3v  29194  elwspths2spth  29218  clwlkclwwlklem2fv2  29246  grpofo  29747  nvss  29841  nmosetn0  30013  hhsst  30514  pjoc1i  30679  chlejb1i  30724  cmbr4i  30849  pjjsi  30948  nmopun  31262  stlesi  31489  mdsl2bi  31571  mdslmd1lem1  31573  xraddge02  31964  supxrnemnf  31976  qtopt1  32810  lmxrge0  32927  esumcst  33056  sigagenval  33133  measdivcstALTV  33218  oms0  33291  ballotlemfc0  33486  ballotlemfcc  33487  bnj945  33779  bnj986  33961  bnj1421  34048  fv1stcnv  34743  fv2ndcnv  34744  fness  35229  nandsym1  35302  bj-finsumval0  36161  finixpnum  36468  poimirlem3  36486  poimirlem16  36499  poimirlem17  36500  poimirlem19  36502  poimirlem20  36503  poimirlem27  36510  ismblfin  36524  lcvexchlem5  37903  paddssat  38680  dibn0  40019  lclkrs2  40406  aks4d1p1p7  40934  eqresfnbd  41056  fiphp3d  41547  pellqrex  41607  jm2.16nn0  41733  onexlimgt  41982  cantnf2  42065  rp-fakeanorass  42254  clsk1indlem2  42783  icccncfext  44593  wallispilem4  44774  fmtnorec1  46195  fmtnoprmfac1lem  46222  mod42tp1mod8  46260  stgoldbwt  46434  sbgoldbwt  46435  sbgoldbst  46436  evengpoap3  46457  wtgoldbnnsum4prm  46460  bgoldbnnsum3prm  46462  pzriprngALT  46809  ply1mulgsumlem2  47058  ldepspr  47144  blennngt2o2  47268  inlinecirc02plem  47462