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  6413  funtp  6597  dmtpos  8255  frrlem11  8314  oaabs2  8658  ixpsnf1o  8966  fodomr  9147  fodomfir  9319  mapfienlem2  9398  cantnfrescl  9677  dfttrcl2  9725  cardprclem  10060  fin4en1  10387  ssfin4  10388  axdc3lem2  10529  axdc3lem4  10531  fpwwe2lem8  10723  recexsrlem  11188  nn0n0n1ge2b  12675  xmulpnf1  13404  ige2m2fzo  13863  swrdlsw  14817  swrd2lsw  15105  wrdl3s3  15115  lcmfass  16821  qredeu  16833  qnumdencoprm  16921  qeqnumdivden  16922  isacs1i  17831  subgga  19514  symgfixf1  19651  sylow1lem2  19813  sylow3lem1  19841  nn0gsumfz  20198  pzriprngALT  21801  evlsgsumadd  22405  evlsgsummul  22406  mhpmulcl  22470  mptcoe1fsupp  22533  evls1gsumadd  22642  evls1gsummul  22643  evl1gsummul  22678  mat1scmat  22854  smadiadetlem4  22984  mptcoe1matfsupp  23120  chfacfscmulgsum  23178  chfacfpmmulgsum  23182  topbas  23290  neips  23431  lmbrf  23578  rnelfm  24272  tsmsres  24463  reconnlem1  25146  lmmbrf  25583  iscauf  25601  caucfil  25604  cmetcaulem  25609  voliunlem1  25871  isosctrlem1  27146  bcmono  27604  2lgslem1a  27718  dchrvmasumlem2  27825  mulog2sumlem2  27862  pntlemb  27924  nodense  28049  conway  28165  etaslts  28179  lesrec  28185  cofcutr  28310  precsexlem9  28601  usgr2pthlem  30349  2pthon3v  30532  elwspths2spth  30559  clwlkclwwlklem2fv2  30587  grpofo  31101  nvss  31195  nmosetn0  31367  hhsst  31868  pjoc1i  32033  chlejb1i  32078  cmbr4i  32203  pjjsi  32302  nmopun  32616  stlesi  32843  mdsl2bi  32925  mdslmd1lem1  32927  xraddge02  33349  supxrnemnf  33360  evlextv  34174  constrextdg2  34381  qtopt1  34467  lmxrge0  34584  esumcst  34695  sigagenval  34773  measdivcstALTV  34858  oms0  34929  ballotlemfc0  35125  ballotlemfcc  35126  bnj945  35404  bnj986  35585  bnj1421  35672  fv1stcnv  36541  fv2ndcnv  36542  fness  37137  nandsym1  37210  bj-finsumval0  38206  finixpnum  38528  poimirlem3  38541  poimirlem16  38554  poimirlem17  38555  poimirlem19  38557  poimirlem20  38558  poimirlem27  38565  ismblfin  38579  ecxrn2  39340  lcvexchlem5  40095  paddssat  40871  dibn0  42210  lclkrs2  42597  aks4d1p1p7  43124  eqresfnbd  43286  fiphp3d  43825  pellqrex  43885  jm2.16nn0  44010  onexlimgt  44244  cantnf2  44326  rp-fakeanorass  44513  clsk1indlem2  45041  icccncfext  46896  wallispilem4  47077  fmtnorec1  48621  fmtnoprmfac1lem  48648  mod42tp1mod8  48686  stgoldbwt  48873  sbgoldbwt  48874  sbgoldbst  48875  evengpoap3  48896  wtgoldbnnsum4prm  48899  bgoldbnnsum3prm  48901  isubgruhgr  48965  uhgrimisgrgric  49028  isubgr3stgrlem7  49069  gpgprismgr4cycl0  49203  ply1mulgsumlem2  49498  ldepspr  49584  blennngt2o2  49703  inlinecirc02plem  49897