Theorem jctir 523

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  jctr  527  ordunidif  6233  funtp  6405  dmtpos  7898  oaabs2  8266  ixpsnf1o  8496  fodomr  8662  mapfienlem2  8863  cantnfrescl  9133  cardprclem  9402  fin4en1  9725  ssfin4  9726  axdc3lem2  9867  axdc3lem4  9869  fpwwe2lem9  10054  recexsrlem  10519  nn0n0n1ge2b  11957  xmulpnf1  12661  ige2m2fzo  13094  swrdlsw  14023  swrd2lsw  14308  wrdl3s3  14320  lcmfass  15984  qredeu  15996  qnumdencoprm  16079  qeqnumdivden  16080  isacs1i  16922  subgga  18424  symgfixf1  18559  sylow1lem2  18718  sylow3lem1  18746  nn0gsumfz  19098  evlsgsumadd  20298  evlsgsummul  20299  mptcoe1fsupp  20377  evls1gsumadd  20481  evls1gsummul  20482  evl1gsummul  20517  mat1scmat  21142  smadiadetlem4  21272  mptcoe1matfsupp  21404  chfacfscmulgsum  21462  chfacfpmmulgsum  21466  topbas  21574  neips  21715  lmbrf  21862  rnelfm  22555  tsmsres  22746  reconnlem1  23428  lmmbrf  23859  iscauf  23877  caucfil  23880  cmetcaulem  23885  voliunlem1  24145  isosctrlem1  25390  bcmono  25847  2lgslem1a  25961  dchrvmasumlem2  26068  mulog2sumlem2  26105  pntlemb  26167  usgr2pthlem  27538  2pthon3v  27716  elwspths2spth  27740  clwlkclwwlklem2fv2  27768  grpofo  28270  nvss  28364  nmosetn0  28536  hhsst  29037  pjoc1i  29202  chlejb1i  29247  cmbr4i  29372  pjjsi  29471  nmopun  29785  stlesi  30012  mdsl2bi  30094  mdslmd1lem1  30096  xraddge02  30474  supxrnemnf  30487  qtopt1  31094  lmxrge0  31190  esumcst  31317  sigagenval  31394  measdivcstALTV  31479  oms0  31550  ballotlemfc0  31745  ballotlemfcc  31746  bnj945  32040  bnj986  32222  bnj1421  32309  fv1stcnv  33015  fv2ndcnv  33016  dftrpred3g  33067  frrlem11  33128  nodense  33191  nulssgt  33258  conway  33259  etasslt  33269  slerec  33272  fness  33692  nandsym1  33765  bj-finsumval0  34561  finixpnum  34871  poimirlem3  34889  poimirlem16  34902  poimirlem17  34903  poimirlem19  34905  poimirlem20  34906  poimirlem27  34913  ismblfin  34927  lcvexchlem5  36168  paddssat  36944  dibn0  38283  lclkrs2  38670  fiphp3d  39409  pellqrex  39469  jm2.16nn0  39594  rp-fakeanorass  39872  clsk1indlem2  40385  icccncfext  42163  wallispilem4  42347  fmtnorec1  43693  fmtnoprmfac1lem  43720  mod42tp1mod8  43761  stgoldbwt  43935  sbgoldbwt  43936  sbgoldbst  43937  evengpoap3  43958  wtgoldbnnsum4prm  43961  bgoldbnnsum3prm  43963  ply1mulgsumlem2  44435  ldepspr  44522  blennngt2o2  44646  inlinecirc02plem  44767