Theorem jctir 525

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  jctr  529  ordunidif  6360  funtp  6542  dmtpos  8178  frrlem11  8236  oaabs2  8575  ixpsnf1o  8876  fodomr  9056  fodomfir  9228  mapfienlem2  9309  cantnfrescl  9588  dfttrcl2  9636  cardprclem  9894  fin4en1  10222  ssfin4  10223  axdc3lem2  10364  axdc3lem4  10366  fpwwe2lem8  10552  recexsrlem  11017  nn0n0n1ge2b  12497  xmulpnf1  13217  ige2m2fzo  13674  swrdlsw  14621  swrd2lsw  14905  wrdl3s3  14915  lcmfass  16606  qredeu  16618  qnumdencoprm  16706  qeqnumdivden  16707  isacs1i  17614  subgga  19266  symgfixf1  19403  sylow1lem2  19565  sylow3lem1  19593  nn0gsumfz  19950  pzriprngALT  21470  evlsgsumadd  22072  evlsgsummul  22073  mhpmulcl  22137  mptcoe1fsupp  22200  evls1gsumadd  22310  evls1gsummul  22311  evl1gsummul  22346  mat1scmat  22522  smadiadetlem4  22652  mptcoe1matfsupp  22785  chfacfscmulgsum  22843  chfacfpmmulgsum  22847  topbas  22955  neips  23096  lmbrf  23243  rnelfm  23936  tsmsres  24127  reconnlem1  24810  lmmbrf  25247  iscauf  25265  caucfil  25268  cmetcaulem  25273  voliunlem1  25535  isosctrlem1  26800  bcmono  27258  2lgslem1a  27372  dchrvmasumlem2  27479  mulog2sumlem2  27516  pntlemb  27578  nodense  27674  conway  27789  etaslts  27803  lesrec  27809  cofcutr  27934  precsexlem9  28225  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  32849  supxrnemnf  32860  evlextv  33726  constrextdg2  33933  qtopt1  34019  lmxrge0  34136  esumcst  34247  sigagenval  34324  measdivcstALTV  34409  oms0  34481  ballotlemfc0  34677  ballotlemfcc  34678  bnj945  34956  bnj986  35137  bnj1421  35224  fv1stcnv  36005  fv2ndcnv  36006  fness  36577  nandsym1  36650  bj-finsumval0  37645  finixpnum  37972  poimirlem3  37990  poimirlem16  38003  poimirlem17  38004  poimirlem19  38006  poimirlem20  38007  poimirlem27  38014  ismblfin  38028  ecxrn2  38775  lcvexchlem5  39530  paddssat  40306  dibn0  41645  lclkrs2  42032  aks4d1p1p7  42559  eqresfnbd  42719  fiphp3d  43264  pellqrex  43324  jm2.16nn0  43449  onexlimgt  43688  cantnf2  43770  rp-fakeanorass  43957  clsk1indlem2  44486  icccncfext  46330  wallispilem4  46511  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