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  6434  funtp  6624  dmtpos  8261  frrlem11  8319  oaabs2  8685  ixpsnf1o  8976  fodomr  9166  fodomfir  9365  mapfienlem2  9443  cantnfrescl  9713  dfttrcl2  9761  cardprclem  10016  fin4en1  10346  ssfin4  10347  axdc3lem2  10488  axdc3lem4  10490  fpwwe2lem8  10675  recexsrlem  11140  nn0n0n1ge2b  12592  xmulpnf1  13312  ige2m2fzo  13763  swrdlsw  14701  swrd2lsw  14987  wrdl3s3  14997  lcmfass  16679  qredeu  16691  qnumdencoprm  16778  qeqnumdivden  16779  isacs1i  17701  subgga  19330  symgfixf1  19469  sylow1lem2  19631  sylow3lem1  19659  nn0gsumfz  20016  pzriprngALT  21523  evlsgsumadd  22132  evlsgsummul  22133  mhpmulcl  22170  mptcoe1fsupp  22232  evls1gsumadd  22343  evls1gsummul  22344  evl1gsummul  22379  mat1scmat  22560  smadiadetlem4  22690  mptcoe1matfsupp  22823  chfacfscmulgsum  22881  chfacfpmmulgsum  22885  topbas  22994  neips  23136  lmbrf  23283  rnelfm  23976  tsmsres  24167  reconnlem1  24861  lmmbrf  25309  iscauf  25327  caucfil  25330  cmetcaulem  25335  voliunlem1  25598  isosctrlem1  26875  bcmono  27335  2lgslem1a  27449  dchrvmasumlem2  27556  mulog2sumlem2  27593  pntlemb  27655  nodense  27751  conway  27858  etasslt  27872  slerec  27878  cofcutr  27972  precsexlem9  28253  usgr2pthlem  29795  2pthon3v  29972  elwspths2spth  29996  clwlkclwwlklem2fv2  30024  grpofo  30527  nvss  30621  nmosetn0  30793  hhsst  31294  pjoc1i  31459  chlejb1i  31504  cmbr4i  31629  pjjsi  31728  nmopun  32042  stlesi  32269  mdsl2bi  32351  mdslmd1lem1  32353  xraddge02  32766  supxrnemnf  32778  qtopt1  33795  lmxrge0  33912  esumcst  34043  sigagenval  34120  measdivcstALTV  34205  oms0  34278  ballotlemfc0  34473  ballotlemfcc  34474  bnj945  34765  bnj986  34947  bnj1421  35034  fv1stcnv  35757  fv2ndcnv  35758  fness  36331  nandsym1  36404  bj-finsumval0  37267  finixpnum  37591  poimirlem3  37609  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  poimirlem27  37633  ismblfin  37647  lcvexchlem5  39019  paddssat  39796  dibn0  41135  lclkrs2  41522  aks4d1p1p7  42055  eqresfnbd  42251  fiphp3d  42806  pellqrex  42866  jm2.16nn0  42992  onexlimgt  43231  cantnf2  43314  rp-fakeanorass  43502  clsk1indlem2  44031  icccncfext  45842  wallispilem4  46023  fmtnorec1  47461  fmtnoprmfac1lem  47488  mod42tp1mod8  47526  stgoldbwt  47700  sbgoldbwt  47701  sbgoldbst  47702  evengpoap3  47723  wtgoldbnnsum4prm  47726  bgoldbnnsum3prm  47728  isubgruhgr  47791  uhgrimisgrgric  47836  isubgr3stgrlem7  47874  ply1mulgsumlem2  48232  ldepspr  48318  blennngt2o2  48441  inlinecirc02plem  48635