Theorem jctir 524

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  jctr  528  ordunidif  6207  funtp  6381  dmtpos  7887  oaabs2  8255  ixpsnf1o  8485  fodomr  8652  mapfienlem2  8853  cantnfrescl  9123  cardprclem  9392  fin4en1  9720  ssfin4  9721  axdc3lem2  9862  axdc3lem4  9864  fpwwe2lem9  10049  recexsrlem  10514  nn0n0n1ge2b  11951  xmulpnf1  12655  ige2m2fzo  13095  swrdlsw  14020  swrd2lsw  14305  wrdl3s3  14317  lcmfass  15980  qredeu  15992  qnumdencoprm  16075  qeqnumdivden  16076  isacs1i  16920  subgga  18422  symgfixf1  18557  sylow1lem2  18716  sylow3lem1  18744  nn0gsumfz  19097  evlsgsumadd  20763  evlsgsummul  20764  mptcoe1fsupp  20844  evls1gsumadd  20948  evls1gsummul  20949  evl1gsummul  20984  mat1scmat  21144  smadiadetlem4  21274  mptcoe1matfsupp  21407  chfacfscmulgsum  21465  chfacfpmmulgsum  21469  topbas  21577  neips  21718  lmbrf  21865  rnelfm  22558  tsmsres  22749  reconnlem1  23431  lmmbrf  23866  iscauf  23884  caucfil  23887  cmetcaulem  23892  voliunlem1  24154  isosctrlem1  25404  bcmono  25861  2lgslem1a  25975  dchrvmasumlem2  26082  mulog2sumlem2  26119  pntlemb  26181  usgr2pthlem  27552  2pthon3v  27729  elwspths2spth  27753  clwlkclwwlklem2fv2  27781  grpofo  28282  nvss  28376  nmosetn0  28548  hhsst  29049  pjoc1i  29214  chlejb1i  29259  cmbr4i  29384  pjjsi  29483  nmopun  29797  stlesi  30024  mdsl2bi  30106  mdslmd1lem1  30108  xraddge02  30506  supxrnemnf  30519  qtopt1  31188  lmxrge0  31305  esumcst  31432  sigagenval  31509  measdivcstALTV  31594  oms0  31665  ballotlemfc0  31860  ballotlemfcc  31861  bnj945  32155  bnj986  32337  bnj1421  32424  fv1stcnv  33133  fv2ndcnv  33134  dftrpred3g  33185  frrlem11  33246  nodense  33309  nulssgt  33376  conway  33377  etasslt  33387  slerec  33390  fness  33810  nandsym1  33883  bj-finsumval0  34700  finixpnum  35042  poimirlem3  35060  poimirlem16  35073  poimirlem17  35074  poimirlem19  35076  poimirlem20  35077  poimirlem27  35084  ismblfin  35098  lcvexchlem5  36334  paddssat  37110  dibn0  38449  lclkrs2  38836  fiphp3d  39760  pellqrex  39820  jm2.16nn0  39945  rp-fakeanorass  40221  clsk1indlem2  40745  icccncfext  42529  wallispilem4  42710  fmtnorec1  44054  fmtnoprmfac1lem  44081  mod42tp1mod8  44120  stgoldbwt  44294  sbgoldbwt  44295  sbgoldbst  44296  evengpoap3  44317  wtgoldbnnsum4prm  44320  bgoldbnnsum3prm  44322  ply1mulgsumlem2  44795  ldepspr  44882  blennngt2o2  45006  inlinecirc02plem  45200