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  6367  funtp  6549  dmtpos  8180  frrlem11  8238  oaabs2  8577  ixpsnf1o  8876  fodomr  9056  fodomfir  9228  mapfienlem2  9309  cantnfrescl  9585  dfttrcl2  9633  cardprclem  9891  fin4en1  10219  ssfin4  10220  axdc3lem2  10361  axdc3lem4  10363  fpwwe2lem8  10549  recexsrlem  11014  nn0n0n1ge2b  12470  xmulpnf1  13189  ige2m2fzo  13644  swrdlsw  14591  swrd2lsw  14875  wrdl3s3  14885  lcmfass  16573  qredeu  16585  qnumdencoprm  16672  qeqnumdivden  16673  isacs1i  17580  subgga  19229  symgfixf1  19366  sylow1lem2  19528  sylow3lem1  19556  nn0gsumfz  19913  pzriprngALT  21450  evlsgsumadd  22051  evlsgsummul  22052  mhpmulcl  22092  mptcoe1fsupp  22156  evls1gsumadd  22268  evls1gsummul  22269  evl1gsummul  22304  mat1scmat  22483  smadiadetlem4  22613  mptcoe1matfsupp  22746  chfacfscmulgsum  22804  chfacfpmmulgsum  22808  topbas  22916  neips  23057  lmbrf  23204  rnelfm  23897  tsmsres  24088  reconnlem1  24771  lmmbrf  25218  iscauf  25236  caucfil  25239  cmetcaulem  25244  voliunlem1  25507  isosctrlem1  26784  bcmono  27244  2lgslem1a  27358  dchrvmasumlem2  27465  mulog2sumlem2  27502  pntlemb  27564  nodense  27660  conway  27775  etaslts  27789  lesrec  27795  cofcutr  27920  precsexlem9  28211  usgr2pthlem  29836  2pthon3v  30016  elwspths2spth  30043  clwlkclwwlklem2fv2  30071  grpofo  30574  nvss  30668  nmosetn0  30840  hhsst  31341  pjoc1i  31506  chlejb1i  31551  cmbr4i  31676  pjjsi  31775  nmopun  32089  stlesi  32316  mdsl2bi  32398  mdslmd1lem1  32400  xraddge02  32837  supxrnemnf  32848  evlextv  33707  constrextdg2  33906  qtopt1  33992  lmxrge0  34109  esumcst  34220  sigagenval  34297  measdivcstALTV  34382  oms0  34454  ballotlemfc0  34650  ballotlemfcc  34651  bnj945  34929  bnj986  35111  bnj1421  35198  fv1stcnv  35971  fv2ndcnv  35972  fness  36543  nandsym1  36616  bj-finsumval0  37490  finixpnum  37806  poimirlem3  37824  poimirlem16  37837  poimirlem17  37838  poimirlem19  37840  poimirlem20  37841  poimirlem27  37848  ismblfin  37862  ecxrn2  38593  lcvexchlem5  39298  paddssat  40074  dibn0  41413  lclkrs2  41800  aks4d1p1p7  42328  eqresfnbd  42488  fiphp3d  43061  pellqrex  43121  jm2.16nn0  43246  onexlimgt  43485  cantnf2  43567  rp-fakeanorass  43754  clsk1indlem2  44283  icccncfext  46131  wallispilem4  46312  fmtnorec1  47783  fmtnoprmfac1lem  47810  mod42tp1mod8  47848  stgoldbwt  48022  sbgoldbwt  48023  sbgoldbst  48024  evengpoap3  48045  wtgoldbnnsum4prm  48048  bgoldbnnsum3prm  48050  isubgruhgr  48114  uhgrimisgrgric  48177  isubgr3stgrlem7  48218  gpgprismgr4cycl0  48352  ply1mulgsumlem2  48633  ldepspr  48719  blennngt2o2  48838  inlinecirc02plem  49032