Theorem jctir 510

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

Syntax hints:   → wi 4   ∧ wa 382

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 197  df-an 383

This theorem is referenced by:  jctr  514  uniintsn  4648  ordunidif  5916  funtp  6086  foimacnv  6295  respreima  6487  fpr  6564  curry1  7420  dmtpos  7516  wfrlem13  7580  oawordeulem  7788  oelim2  7829  oaabs2  7879  ixpsnf1o  8102  ssdomg  8155  fodomr  8267  limenpsi  8291  cantnfrescl  8737  cardprclem  9005  fin4en1  9333  ssfin4  9334  axdc3lem2  9475  axdc3lem4  9477  fpwwe2lem9  9662  reclem2pr  10072  recexsrlem  10126  nn0n0n1ge2b  11561  xmulpnf1  12309  ige2m2fzo  12739  swrdlsw  13661  swrd2lsw  13905  wrdl3s3  13915  climeu  14494  algcvgblem  15498  lcmfass  15567  qredeu  15579  qnumdencoprm  15660  qeqnumdivden  15661  isacs1i  16525  subgga  17940  symgfixf1  18064  sylow1lem2  18221  sylow3lem1  18249  nn0gsumfz  18587  mptcoe1fsupp  19800  evls1gsumadd  19904  evls1gsummul  19905  evl1gsummul  19939  mat1scmat  20563  smadiadetlem4  20694  mptcoe1matfsupp  20827  chfacfscmulgsum  20885  chfacfpmmulgsum  20889  eltg3i  20986  topbas  20997  neips  21138  lmbrf  21285  rnelfm  21977  tsmsres  22167  reconnlem1  22849  lmmbrf  23279  iscauf  23297  caucfil  23300  cmetcaulem  23305  voliunlem1  23538  isosctrlem1  24769  bcmono  25223  2lgslem1a  25337  dchrvmasumlem2  25408  mulog2sumlem2  25445  pntlemb  25507  axlowdimlem13  26055  usgr2pthlem  26894  2pthon3v  27090  elwspths2spth  27116  clwwlkccatlem  27139  clwlkclwwlklem2fv2  27146  clwlksf1clwwlkOLD  27250  grpofo  27693  nvss  27788  nmosetn0  27960  hhsst  28463  pjoc1i  28630  chlejb1i  28675  cmbr4i  28800  pjjsi  28899  nmopun  29213  stlesi  29440  mdsl2bi  29522  mdslmd1lem1  29524  xraddge02  29861  supxrnemnf  29874  qtopt1  30242  lmxrge0  30338  esumcst  30465  sigagenval  30543  measdivcstOLD  30627  oms0  30699  ballotlemfc0  30894  ballotlemfcc  30895  bnj945  31182  bnj150  31284  bnj986  31362  bnj1421  31448  dftrpred3g  32069  nodense  32179  nulssgt  32246  conway  32247  etasslt  32257  slerec  32260  fness  32681  nandsym1  32758  bj-finsumval0  33484  finixpnum  33727  poimirlem3  33745  poimirlem16  33758  poimirlem17  33759  poimirlem19  33761  poimirlem20  33762  poimirlem27  33769  ismblfin  33783  rngoideu  34034  lcvexchlem5  34847  paddssat  35622  dibn0  36963  lclkrs2  37350  fiphp3d  37909  pellqrex  37969  jm2.16nn0  38097  rp-fakeanorass  38384  clsk1indlem2  38866  icccncfext  40618  wallispilem4  40802  fmtnorec1  41977  fmtnoprmfac1lem  42004  mod42tp1mod8  42047  stgoldbwt  42192  sbgoldbwt  42193  sbgoldbst  42194  evengpoap3  42215  wtgoldbnnsum4prm  42218  bgoldbnnsum3prm  42220  ply1mulgsumlem2  42703  ldepspr  42790  blennngt2o2  42914