Theorem jctir 529

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  jctr  533  ordunidif  6412  funtp  6594  dmtpos  8233  frrlem11  8292  oaabs2  8634  ixpsnf1o  8935  fodomr  9115  fodomfir  9286  mapfienlem2  9365  cantnfrescl  9644  dfttrcl2  9692  cardprclem  9964  fin4en1  10292  ssfin4  10293  axdc3lem2  10434  axdc3lem4  10436  fpwwe2lem8  10622  recexsrlem  11087  nn0n0n1ge2b  12572  xmulpnf1  13299  ige2m2fzo  13756  swrdlsw  14704  swrd2lsw  14988  wrdl3s3  14998  lcmfass  16703  qredeu  16715  qnumdencoprm  16803  qeqnumdivden  16804  isacs1i  17712  subgga  19369  symgfixf1  19506  sylow1lem2  19668  sylow3lem1  19696  nn0gsumfz  20053  pzriprngALT  21613  evlsgsumadd  22215  evlsgsummul  22216  mhpmulcl  22280  mptcoe1fsupp  22343  evls1gsumadd  22452  evls1gsummul  22453  evl1gsummul  22488  mat1scmat  22664  smadiadetlem4  22794  mptcoe1matfsupp  22927  chfacfscmulgsum  22985  chfacfpmmulgsum  22989  topbas  23097  neips  23238  lmbrf  23385  rnelfm  24078  tsmsres  24269  reconnlem1  24952  lmmbrf  25389  iscauf  25407  caucfil  25410  cmetcaulem  25415  voliunlem1  25677  isosctrlem1  26948  bcmono  27406  2lgslem1a  27520  dchrvmasumlem2  27627  mulog2sumlem2  27664  pntlemb  27726  nodense  27821  conway  27937  etaslts  27951  lesrec  27957  cofcutr  28082  precsexlem9  28373  usgr2pthlem  30052  2pthon3v  30232  elwspths2spth  30259  clwlkclwwlklem2fv2  30287  grpofo  30791  nvss  30885  nmosetn0  31057  hhsst  31558  pjoc1i  31723  chlejb1i  31768  cmbr4i  31893  pjjsi  31992  nmopun  32306  stlesi  32533  mdsl2bi  32615  mdslmd1lem1  32617  xraddge02  33042  supxrnemnf  33053  evlextv  33876  constrextdg2  34083  qtopt1  34169  lmxrge0  34286  esumcst  34397  sigagenval  34474  measdivcstALTV  34559  oms0  34631  ballotlemfc0  34827  ballotlemfcc  34828  bnj945  35106  bnj986  35287  bnj1421  35374  fv1stcnv  36167  fv2ndcnv  36168  fness  36748  nandsym1  36821  bj-finsumval0  37816  finixpnum  38143  poimirlem3  38161  poimirlem16  38174  poimirlem17  38175  poimirlem19  38177  poimirlem20  38178  poimirlem27  38185  ismblfin  38199  ecxrn2  38946  lcvexchlem5  39701  paddssat  40477  dibn0  41816  lclkrs2  42203  aks4d1p1p7  42730  eqresfnbd  42892  fiphp3d  43437  pellqrex  43497  jm2.16nn0  43622  onexlimgt  43861  cantnf2  43943  rp-fakeanorass  44130  clsk1indlem2  44659  icccncfext  46492  wallispilem4  46673  fmtnorec1  48177  fmtnoprmfac1lem  48204  mod42tp1mod8  48242  stgoldbwt  48429  sbgoldbwt  48430  sbgoldbst  48431  evengpoap3  48452  wtgoldbnnsum4prm  48455  bgoldbnnsum3prm  48457  isubgruhgr  48521  uhgrimisgrgric  48584  isubgr3stgrlem7  48625  gpgprismgr4cycl0  48759  ply1mulgsumlem2  49051  ldepspr  49137  blennngt2o2  49256  inlinecirc02plem  49450