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  6444  funtp  6635  dmtpos  8279  frrlem11  8337  oaabs2  8705  ixpsnf1o  8996  fodomr  9194  fodomfir  9396  mapfienlem2  9475  cantnfrescl  9745  dfttrcl2  9793  cardprclem  10048  fin4en1  10378  ssfin4  10379  axdc3lem2  10520  axdc3lem4  10522  fpwwe2lem8  10707  recexsrlem  11172  nn0n0n1ge2b  12621  xmulpnf1  13336  ige2m2fzo  13779  swrdlsw  14715  swrd2lsw  15001  wrdl3s3  15011  lcmfass  16693  qredeu  16705  qnumdencoprm  16792  qeqnumdivden  16793  isacs1i  17715  subgga  19340  symgfixf1  19479  sylow1lem2  19641  sylow3lem1  19669  nn0gsumfz  20026  pzriprngALT  21529  evlsgsumadd  22138  evlsgsummul  22139  mhpmulcl  22176  mptcoe1fsupp  22238  evls1gsumadd  22349  evls1gsummul  22350  evl1gsummul  22385  mat1scmat  22566  smadiadetlem4  22696  mptcoe1matfsupp  22829  chfacfscmulgsum  22887  chfacfpmmulgsum  22891  topbas  23000  neips  23142  lmbrf  23289  rnelfm  23982  tsmsres  24173  reconnlem1  24867  lmmbrf  25315  iscauf  25333  caucfil  25336  cmetcaulem  25341  voliunlem1  25604  isosctrlem1  26879  bcmono  27339  2lgslem1a  27453  dchrvmasumlem2  27560  mulog2sumlem2  27597  pntlemb  27659  nodense  27755  conway  27862  etasslt  27876  slerec  27882  cofcutr  27976  precsexlem9  28257  usgr2pthlem  29799  2pthon3v  29976  elwspths2spth  30000  clwlkclwwlklem2fv2  30028  grpofo  30531  nvss  30625  nmosetn0  30797  hhsst  31298  pjoc1i  31463  chlejb1i  31508  cmbr4i  31633  pjjsi  31732  nmopun  32046  stlesi  32273  mdsl2bi  32355  mdslmd1lem1  32357  xraddge02  32763  supxrnemnf  32775  qtopt1  33781  lmxrge0  33898  esumcst  34027  sigagenval  34104  measdivcstALTV  34189  oms0  34262  ballotlemfc0  34457  ballotlemfcc  34458  bnj945  34749  bnj986  34931  bnj1421  35018  fv1stcnv  35740  fv2ndcnv  35741  fness  36315  nandsym1  36388  bj-finsumval0  37251  finixpnum  37565  poimirlem3  37583  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem27  37607  ismblfin  37621  lcvexchlem5  38994  paddssat  39771  dibn0  41110  lclkrs2  41497  aks4d1p1p7  42031  eqresfnbd  42227  fiphp3d  42775  pellqrex  42835  jm2.16nn0  42961  onexlimgt  43204  cantnf2  43287  rp-fakeanorass  43475  clsk1indlem2  44004  icccncfext  45808  wallispilem4  45989  fmtnorec1  47411  fmtnoprmfac1lem  47438  mod42tp1mod8  47476  stgoldbwt  47650  sbgoldbwt  47651  sbgoldbst  47652  evengpoap3  47673  wtgoldbnnsum4prm  47676  bgoldbnnsum3prm  47678  isubgruhgr  47738  uhgrimisgrgric  47783  ply1mulgsumlem2  48116  ldepspr  48202  blennngt2o2  48326  inlinecirc02plem  48520