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  6416  funtp  6602  dmtpos  8263  frrlem11  8322  oaabs2  8666  ixpsnf1o  8974  fodomr  9155  fodomfir  9327  mapfienlem2  9405  cantnfrescl  9684  dfttrcl2  9732  cardprclem  10067  fin4en1  10394  ssfin4  10395  axdc3lem2  10536  axdc3lem4  10538  fpwwe2lem8  10730  recexsrlem  11195  nn0n0n1ge2b  12682  xmulpnf1  13411  ige2m2fzo  13870  swrdlsw  14825  swrd2lsw  15114  wrdl3s3  15124  lcmfass  16830  qredeu  16842  qnumdencoprm  16930  qeqnumdivden  16931  isacs1i  17840  subgga  19523  symgfixf1  19660  sylow1lem2  19822  sylow3lem1  19850  nn0gsumfz  20207  pzriprngALT  21810  evlsgsumadd  22414  evlsgsummul  22415  mhpmulcl  22479  mptcoe1fsupp  22542  evls1gsumadd  22651  evls1gsummul  22652  evl1gsummul  22687  mat1scmat  22863  smadiadetlem4  22993  mptcoe1matfsupp  23129  chfacfscmulgsum  23187  chfacfpmmulgsum  23191  topbas  23299  neips  23440  lmbrf  23587  rnelfm  24281  tsmsres  24472  reconnlem1  25155  lmmbrf  25592  iscauf  25610  caucfil  25613  cmetcaulem  25618  voliunlem1  25880  isosctrlem1  27155  bcmono  27613  2lgslem1a  27727  dchrvmasumlem2  27834  mulog2sumlem2  27871  pntlemb  27933  nodense  28058  conway  28174  etaslts  28188  lesrec  28194  cofcutr  28319  precsexlem9  28610  usgr2pthlem  30358  2pthon3v  30541  elwspths2spth  30568  clwlkclwwlklem2fv2  30596  grpofo  31110  nvss  31204  nmosetn0  31376  hhsst  31877  pjoc1i  32042  chlejb1i  32087  cmbr4i  32212  pjjsi  32311  nmopun  32625  stlesi  32852  mdsl2bi  32934  mdslmd1lem1  32936  xraddge02  33399  supxrnemnf  33410  evlextv  34224  constrextdg2  34431  qtopt1  34517  lmxrge0  34634  esumcst  34745  sigagenval  34823  measdivcstALTV  34908  oms0  34979  ballotlemfc0  35175  ballotlemfcc  35176  bnj945  35454  bnj986  35635  bnj1421  35722  wevsev  35992  fv1stcnv  36665  fv2ndcnv  36666  fness  37261  nandsym1  37334  bj-finsumval0  38343  finixpnum  38665  poimirlem3  38678  poimirlem16  38691  poimirlem17  38692  poimirlem19  38694  poimirlem20  38695  poimirlem27  38702  ismblfin  38716  ecxrn2  39477  lcvexchlem5  40232  paddssat  41008  dibn0  42347  lclkrs2  42734  aks4d1p1p7  43261  eqresfnbd  43423  fiphp3d  43963  pellqrex  44023  jm2.16nn0  44148  onexlimgt  44382  cantnf2  44464  rp-fakeanorass  44651  clsk1indlem2  45179  icccncfext  47033  wallispilem4  47214  fmtnorec1  48758  fmtnoprmfac1lem  48785  mod42tp1mod8  48823  stgoldbwt  49010  sbgoldbwt  49011  sbgoldbst  49012  evengpoap3  49033  wtgoldbnnsum4prm  49036  bgoldbnnsum3prm  49038  isubgruhgr  49102  uhgrimisgrgric  49165  isubgr3stgrlem7  49206  gpgprismgr4cycl0  49340  ply1mulgsumlem2  49635  ldepspr  49721  blennngt2o2  49840  par2diag  50916