Theorem jctir 530

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  jctr  534  ordunidif  6439  funtp  6627  dmtpos  8293  frrlem11  8352  oaabs2  8696  ixpsnf1o  9004  fodomr  9185  fodomfir  9357  mapfienlem2  9435  cantnfrescl  9714  dfttrcl2  9762  cardprclem  10097  fin4en1  10426  ssfin4  10427  axdc3lem2  10568  axdc3lem4  10570  fpwwe2lem8  10762  recexsrlem  11227  nn0n0n1ge2b  12715  xmulpnf1  13444  ige2m2fzo  13903  swrdlsw  14859  swrd2lsw  15148  wrdl3s3  15158  lcmfass  16865  qredeu  16877  qnumdencoprm  16965  qeqnumdivden  16966  isacs1i  17881  subgga  19565  symgfixf1  19702  sylow1lem2  19864  sylow3lem1  19892  nn0gsumfz  20249  pzriprngALT  21856  evlsgsumadd  22460  evlsgsummul  22461  mhpmulcl  22525  mptcoe1fsupp  22588  evls1gsumadd  22697  evls1gsummul  22698  evl1gsummul  22733  mat1scmat  22909  smadiadetlem4  23039  mptcoe1matfsupp  23175  chfacfscmulgsum  23233  chfacfpmmulgsum  23237  topbas  23345  neips  23486  lmbrf  23633  rnelfm  24327  tsmsres  24518  reconnlem1  25201  lmmbrf  25638  iscauf  25656  caucfil  25659  cmetcaulem  25664  voliunlem1  25926  isosctrlem1  27203  bcmono  27661  2lgslem1a  27775  dchrvmasumlem2  27882  mulog2sumlem2  27919  pntlemb  27981  nodense  28106  conway  28222  etaslts  28236  lesrec  28242  cofcutr  28367  precsexlem9  28658  usgr2pthlem  30406  2pthon3v  30589  elwspths2spth  30616  clwlkclwwlklem2fv2  30644  grpofo  31158  nvss  31252  nmosetn0  31424  hhsst  31925  pjoc1i  32090  chlejb1i  32135  cmbr4i  32260  pjjsi  32359  nmopun  32673  stlesi  32900  mdsl2bi  32982  mdslmd1lem1  32984  xraddge02  33445  supxrnemnf  33456  evlextv  34285  constrextdg2  34492  qtopt1  34578  lmxrge0  34695  esumcst  34806  sigagenval  34884  measdivcstALTV  34969  oms0  35040  ballotlemfc0  35236  ballotlemfcc  35237  bnj945  35515  bnj986  35696  bnj1421  35783  wevsev  36082  fv1stcnv  36756  fv2ndcnv  36757  fness  37352  nandsym1  37425  bj-finsumval0  38474  finixpnum  38796  poimirlem3  38809  poimirlem16  38822  poimirlem17  38823  poimirlem19  38825  poimirlem20  38826  poimirlem27  38833  ismblfin  38847  ecxrn2  39606  lcvexchlem5  40361  paddssat  41137  dibn0  42476  lclkrs2  42863  aks4d1p1p7  43390  eqresfnbd  43553  fiphp3d  44092  pellqrex  44152  jm2.16nn0  44277  onexlimgt  44506  cantnf2  44588  rp-fakeanorass  44775  clsk1indlem2  45303  icccncfext  47170  wallispilem4  47351  fmtnorec1  48895  fmtnoprmfac1lem  48922  mod42tp1mod8  48960  stgoldbwt  49147  sbgoldbwt  49148  sbgoldbst  49149  evengpoap3  49170  wtgoldbnnsum4prm  49173  bgoldbnnsum3prm  49175  isubgruhgr  49239  uhgrimisgrgric  49302  isubgr3stgrlem7  49343  gpgprismgr4cycl0  49477  ply1mulgsumlem2  49830  ldepspr  49916  blennngt2o2  50035  par2diag  51111