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  6368  funtp  6550  dmtpos  8182  frrlem11  8240  oaabs2  8579  ixpsnf1o  8880  fodomr  9060  fodomfir  9232  mapfienlem2  9313  cantnfrescl  9591  dfttrcl2  9639  cardprclem  9897  fin4en1  10225  ssfin4  10226  axdc3lem2  10367  axdc3lem4  10369  fpwwe2lem8  10555  recexsrlem  11020  nn0n0n1ge2b  12500  xmulpnf1  13220  ige2m2fzo  13677  swrdlsw  14624  swrd2lsw  14908  wrdl3s3  14918  lcmfass  16609  qredeu  16621  qnumdencoprm  16709  qeqnumdivden  16710  isacs1i  17617  subgga  19269  symgfixf1  19406  sylow1lem2  19568  sylow3lem1  19596  nn0gsumfz  19953  pzriprngALT  21488  evlsgsumadd  22087  evlsgsummul  22088  mhpmulcl  22128  mptcoe1fsupp  22192  evls1gsumadd  22302  evls1gsummul  22303  evl1gsummul  22338  mat1scmat  22517  smadiadetlem4  22647  mptcoe1matfsupp  22780  chfacfscmulgsum  22838  chfacfpmmulgsum  22842  topbas  22950  neips  23091  lmbrf  23238  rnelfm  23931  tsmsres  24122  reconnlem1  24805  lmmbrf  25242  iscauf  25260  caucfil  25263  cmetcaulem  25268  voliunlem1  25530  isosctrlem1  26798  bcmono  27257  2lgslem1a  27371  dchrvmasumlem2  27478  mulog2sumlem2  27515  pntlemb  27577  nodense  27673  conway  27788  etaslts  27802  lesrec  27808  cofcutr  27933  precsexlem9  28224  usgr2pthlem  29849  2pthon3v  30029  elwspths2spth  30056  clwlkclwwlklem2fv2  30084  grpofo  30588  nvss  30682  nmosetn0  30854  hhsst  31355  pjoc1i  31520  chlejb1i  31565  cmbr4i  31690  pjjsi  31789  nmopun  32103  stlesi  32330  mdsl2bi  32412  mdslmd1lem1  32414  xraddge02  32848  supxrnemnf  32859  evlextv  33704  constrextdg2  33912  qtopt1  33998  lmxrge0  34115  esumcst  34226  sigagenval  34303  measdivcstALTV  34388  oms0  34460  ballotlemfc0  34656  ballotlemfcc  34657  bnj945  34935  bnj986  35116  bnj1421  35203  fv1stcnv  35978  fv2ndcnv  35979  fness  36550  nandsym1  36623  bj-finsumval0  37618  finixpnum  37943  poimirlem3  37961  poimirlem16  37974  poimirlem17  37975  poimirlem19  37977  poimirlem20  37978  poimirlem27  37985  ismblfin  37999  ecxrn2  38746  lcvexchlem5  39501  paddssat  40277  dibn0  41616  lclkrs2  42003  aks4d1p1p7  42530  eqresfnbd  42690  fiphp3d  43268  pellqrex  43328  jm2.16nn0  43453  onexlimgt  43692  cantnf2  43774  rp-fakeanorass  43961  clsk1indlem2  44490  icccncfext  46336  wallispilem4  46517  fmtnorec1  48015  fmtnoprmfac1lem  48042  mod42tp1mod8  48080  stgoldbwt  48267  sbgoldbwt  48268  sbgoldbst  48269  evengpoap3  48290  wtgoldbnnsum4prm  48293  bgoldbnnsum3prm  48295  isubgruhgr  48359  uhgrimisgrgric  48422  isubgr3stgrlem7  48463  gpgprismgr4cycl0  48597  ply1mulgsumlem2  48878  ldepspr  48964  blennngt2o2  49083  inlinecirc02plem  49277