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  6365  funtp  6547  dmtpos  8178  frrlem11  8236  oaabs2  8575  ixpsnf1o  8874  fodomr  9054  fodomfir  9226  mapfienlem2  9307  cantnfrescl  9583  dfttrcl2  9631  cardprclem  9889  fin4en1  10217  ssfin4  10218  axdc3lem2  10359  axdc3lem4  10361  fpwwe2lem8  10547  recexsrlem  11012  nn0n0n1ge2b  12468  xmulpnf1  13187  ige2m2fzo  13642  swrdlsw  14589  swrd2lsw  14873  wrdl3s3  14883  lcmfass  16571  qredeu  16583  qnumdencoprm  16670  qeqnumdivden  16671  isacs1i  17578  subgga  19227  symgfixf1  19364  sylow1lem2  19526  sylow3lem1  19554  nn0gsumfz  19911  pzriprngALT  21448  evlsgsumadd  22049  evlsgsummul  22050  mhpmulcl  22090  mptcoe1fsupp  22154  evls1gsumadd  22266  evls1gsummul  22267  evl1gsummul  22302  mat1scmat  22481  smadiadetlem4  22611  mptcoe1matfsupp  22744  chfacfscmulgsum  22802  chfacfpmmulgsum  22806  topbas  22914  neips  23055  lmbrf  23202  rnelfm  23895  tsmsres  24086  reconnlem1  24769  lmmbrf  25216  iscauf  25234  caucfil  25237  cmetcaulem  25242  voliunlem1  25505  isosctrlem1  26782  bcmono  27242  2lgslem1a  27356  dchrvmasumlem2  27463  mulog2sumlem2  27500  pntlemb  27562  nodense  27658  conway  27767  etasslt  27781  slerec  27787  cofcutr  27895  precsexlem9  28183  usgr2pthlem  29785  2pthon3v  29965  elwspths2spth  29992  clwlkclwwlklem2fv2  30020  grpofo  30523  nvss  30617  nmosetn0  30789  hhsst  31290  pjoc1i  31455  chlejb1i  31500  cmbr4i  31625  pjjsi  31724  nmopun  32038  stlesi  32265  mdsl2bi  32347  mdslmd1lem1  32349  xraddge02  32786  supxrnemnf  32797  evlextv  33656  constrextdg2  33855  qtopt1  33941  lmxrge0  34058  esumcst  34169  sigagenval  34246  measdivcstALTV  34331  oms0  34403  ballotlemfc0  34599  ballotlemfcc  34600  bnj945  34878  bnj986  35060  bnj1421  35147  fv1stcnv  35920  fv2ndcnv  35921  fness  36492  nandsym1  36565  bj-finsumval0  37429  finixpnum  37745  poimirlem3  37763  poimirlem16  37776  poimirlem17  37777  poimirlem19  37779  poimirlem20  37780  poimirlem27  37787  ismblfin  37801  ecxrn2  38532  lcvexchlem5  39237  paddssat  40013  dibn0  41352  lclkrs2  41739  aks4d1p1p7  42267  eqresfnbd  42430  fiphp3d  43003  pellqrex  43063  jm2.16nn0  43188  onexlimgt  43427  cantnf2  43509  rp-fakeanorass  43696  clsk1indlem2  44225  icccncfext  46073  wallispilem4  46254  fmtnorec1  47725  fmtnoprmfac1lem  47752  mod42tp1mod8  47790  stgoldbwt  47964  sbgoldbwt  47965  sbgoldbst  47966  evengpoap3  47987  wtgoldbnnsum4prm  47990  bgoldbnnsum3prm  47992  isubgruhgr  48056  uhgrimisgrgric  48119  isubgr3stgrlem7  48160  gpgprismgr4cycl0  48294  ply1mulgsumlem2  48575  ldepspr  48661  blennngt2o2  48780  inlinecirc02plem  48974