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  6356  funtp  6538  dmtpos  8168  frrlem11  8226  oaabs2  8564  ixpsnf1o  8862  fodomr  9041  fodomfir  9212  mapfienlem2  9290  cantnfrescl  9566  dfttrcl2  9614  cardprclem  9872  fin4en1  10200  ssfin4  10201  axdc3lem2  10342  axdc3lem4  10344  fpwwe2lem8  10529  recexsrlem  10994  nn0n0n1ge2b  12450  xmulpnf1  13173  ige2m2fzo  13628  swrdlsw  14575  swrd2lsw  14859  wrdl3s3  14869  lcmfass  16557  qredeu  16569  qnumdencoprm  16656  qeqnumdivden  16657  isacs1i  17563  subgga  19212  symgfixf1  19349  sylow1lem2  19511  sylow3lem1  19539  nn0gsumfz  19896  pzriprngALT  21432  evlsgsumadd  22026  evlsgsummul  22027  mhpmulcl  22064  mptcoe1fsupp  22128  evls1gsumadd  22239  evls1gsummul  22240  evl1gsummul  22275  mat1scmat  22454  smadiadetlem4  22584  mptcoe1matfsupp  22717  chfacfscmulgsum  22775  chfacfpmmulgsum  22779  topbas  22887  neips  23028  lmbrf  23175  rnelfm  23868  tsmsres  24059  reconnlem1  24742  lmmbrf  25189  iscauf  25207  caucfil  25210  cmetcaulem  25215  voliunlem1  25478  isosctrlem1  26755  bcmono  27215  2lgslem1a  27329  dchrvmasumlem2  27436  mulog2sumlem2  27473  pntlemb  27535  nodense  27631  conway  27740  etasslt  27754  slerec  27760  cofcutr  27868  precsexlem9  28153  usgr2pthlem  29741  2pthon3v  29921  elwspths2spth  29948  clwlkclwwlklem2fv2  29976  grpofo  30479  nvss  30573  nmosetn0  30745  hhsst  31246  pjoc1i  31411  chlejb1i  31456  cmbr4i  31581  pjjsi  31680  nmopun  31994  stlesi  32221  mdsl2bi  32303  mdslmd1lem1  32305  xraddge02  32740  supxrnemnf  32751  constrextdg2  33762  qtopt1  33848  lmxrge0  33965  esumcst  34076  sigagenval  34153  measdivcstALTV  34238  oms0  34310  ballotlemfc0  34506  ballotlemfcc  34507  bnj945  34785  bnj986  34967  bnj1421  35054  fv1stcnv  35821  fv2ndcnv  35822  fness  36393  nandsym1  36466  bj-finsumval0  37329  finixpnum  37655  poimirlem3  37673  poimirlem16  37686  poimirlem17  37687  poimirlem19  37689  poimirlem20  37690  poimirlem27  37697  ismblfin  37711  ecxrn2  38442  lcvexchlem5  39147  paddssat  39923  dibn0  41262  lclkrs2  41649  aks4d1p1p7  42177  eqresfnbd  42335  fiphp3d  42922  pellqrex  42982  jm2.16nn0  43107  onexlimgt  43346  cantnf2  43428  rp-fakeanorass  43616  clsk1indlem2  44145  icccncfext  45995  wallispilem4  46176  fmtnorec1  47647  fmtnoprmfac1lem  47674  mod42tp1mod8  47712  stgoldbwt  47886  sbgoldbwt  47887  sbgoldbst  47888  evengpoap3  47909  wtgoldbnnsum4prm  47912  bgoldbnnsum3prm  47914  isubgruhgr  47978  uhgrimisgrgric  48041  isubgr3stgrlem7  48082  gpgprismgr4cycl0  48216  ply1mulgsumlem2  48498  ldepspr  48584  blennngt2o2  48703  inlinecirc02plem  48897