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  6415  funtp  6597  dmtpos  8240  frrlem11  8299  oaabs2  8641  ixpsnf1o  8942  fodomr  9123  fodomfir  9294  mapfienlem2  9373  cantnfrescl  9652  dfttrcl2  9700  cardprclem  9981  fin4en1  10308  ssfin4  10309  axdc3lem2  10450  axdc3lem4  10452  fpwwe2lem8  10638  recexsrlem  11103  nn0n0n1ge2b  12588  xmulpnf1  13316  ige2m2fzo  13774  swrdlsw  14727  swrd2lsw  15013  wrdl3s3  15023  lcmfass  16726  qredeu  16738  qnumdencoprm  16826  qeqnumdivden  16827  isacs1i  17735  subgga  19414  symgfixf1  19551  sylow1lem2  19713  sylow3lem1  19741  nn0gsumfz  20098  pzriprngALT  21695  evlsgsumadd  22297  evlsgsummul  22298  mhpmulcl  22362  mptcoe1fsupp  22425  evls1gsumadd  22534  evls1gsummul  22535  evl1gsummul  22570  mat1scmat  22746  smadiadetlem4  22876  mptcoe1matfsupp  23009  chfacfscmulgsum  23067  chfacfpmmulgsum  23071  topbas  23179  neips  23320  lmbrf  23467  rnelfm  24161  tsmsres  24352  reconnlem1  25035  lmmbrf  25472  iscauf  25490  caucfil  25493  cmetcaulem  25498  voliunlem1  25760  isosctrlem1  27034  bcmono  27492  2lgslem1a  27606  dchrvmasumlem2  27713  mulog2sumlem2  27750  pntlemb  27812  nodense  27907  conway  28023  etaslts  28037  lesrec  28043  cofcutr  28168  precsexlem9  28459  usgr2pthlem  30176  2pthon3v  30359  elwspths2spth  30386  clwlkclwwlklem2fv2  30414  grpofo  30922  nvss  31016  nmosetn0  31188  hhsst  31689  pjoc1i  31854  chlejb1i  31899  cmbr4i  32024  pjjsi  32123  nmopun  32437  stlesi  32664  mdsl2bi  32746  mdslmd1lem1  32748  xraddge02  33172  supxrnemnf  33183  evlextv  33996  constrextdg2  34203  qtopt1  34289  lmxrge0  34406  esumcst  34517  sigagenval  34595  measdivcstALTV  34680  oms0  34752  ballotlemfc0  34948  ballotlemfcc  34949  bnj945  35227  bnj986  35408  bnj1421  35495  fv1stcnv  36306  fv2ndcnv  36307  fness  36917  nandsym1  36990  bj-finsumval0  37986  finixpnum  38313  poimirlem3  38331  poimirlem16  38344  poimirlem17  38345  poimirlem19  38347  poimirlem20  38348  poimirlem27  38355  ismblfin  38369  ecxrn2  39115  lcvexchlem5  39870  paddssat  40646  dibn0  41985  lclkrs2  42372  aks4d1p1p7  42899  eqresfnbd  43061  fiphp3d  43604  pellqrex  43664  jm2.16nn0  43789  onexlimgt  44028  cantnf2  44110  rp-fakeanorass  44297  clsk1indlem2  44826  icccncfext  46659  wallispilem4  46840  fmtnorec1  48347  fmtnoprmfac1lem  48374  mod42tp1mod8  48412  stgoldbwt  48599  sbgoldbwt  48600  sbgoldbst  48601  evengpoap3  48622  wtgoldbnnsum4prm  48625  bgoldbnnsum3prm  48627  isubgruhgr  48691  uhgrimisgrgric  48754  isubgr3stgrlem7  48795  gpgprismgr4cycl0  48929  ply1mulgsumlem2  49224  ldepspr  49310  blennngt2o2  49429  inlinecirc02plem  49623