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 206  df-an 396

This theorem is referenced by:  jctr  524  ordunidif  6299  funtp  6475  dmtpos  8025  frrlem11  8083  oaabs2  8439  ixpsnf1o  8684  fodomr  8864  mapfienlem2  9095  cantnfrescl  9364  dftrpred3g  9412  cardprclem  9668  fin4en1  9996  ssfin4  9997  axdc3lem2  10138  axdc3lem4  10140  fpwwe2lem8  10325  recexsrlem  10790  nn0n0n1ge2b  12231  xmulpnf1  12937  ige2m2fzo  13378  swrdlsw  14308  swrd2lsw  14593  wrdl3s3  14605  lcmfass  16279  qredeu  16291  qnumdencoprm  16377  qeqnumdivden  16378  isacs1i  17283  subgga  18821  symgfixf1  18960  sylow1lem2  19119  sylow3lem1  19147  nn0gsumfz  19500  evlsgsumadd  21211  evlsgsummul  21212  mhpmulcl  21249  mptcoe1fsupp  21296  evls1gsumadd  21400  evls1gsummul  21401  evl1gsummul  21436  mat1scmat  21596  smadiadetlem4  21726  mptcoe1matfsupp  21859  chfacfscmulgsum  21917  chfacfpmmulgsum  21921  topbas  22030  neips  22172  lmbrf  22319  rnelfm  23012  tsmsres  23203  reconnlem1  23895  lmmbrf  24331  iscauf  24349  caucfil  24352  cmetcaulem  24357  voliunlem1  24619  isosctrlem1  25873  bcmono  26330  2lgslem1a  26444  dchrvmasumlem2  26551  mulog2sumlem2  26588  pntlemb  26650  usgr2pthlem  28032  2pthon3v  28209  elwspths2spth  28233  clwlkclwwlklem2fv2  28261  grpofo  28762  nvss  28856  nmosetn0  29028  hhsst  29529  pjoc1i  29694  chlejb1i  29739  cmbr4i  29864  pjjsi  29963  nmopun  30277  stlesi  30504  mdsl2bi  30586  mdslmd1lem1  30588  xraddge02  30981  supxrnemnf  30993  qtopt1  31687  lmxrge0  31804  esumcst  31931  sigagenval  32008  measdivcstALTV  32093  oms0  32164  ballotlemfc0  32359  ballotlemfcc  32360  bnj945  32653  bnj986  32835  bnj1421  32922  fv1stcnv  33657  fv2ndcnv  33658  dfttrcl2  33710  nodense  33822  conway  33920  etasslt  33934  slerec  33940  cofcutr  34019  fness  34465  nandsym1  34538  bj-finsumval0  35383  finixpnum  35689  poimirlem3  35707  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem27  35731  ismblfin  35745  lcvexchlem5  36979  paddssat  37755  dibn0  39094  lclkrs2  39481  aks4d1p1p7  40010  fiphp3d  40557  pellqrex  40617  jm2.16nn0  40742  rp-fakeanorass  41018  clsk1indlem2  41541  icccncfext  43318  wallispilem4  43499  fmtnorec1  44877  fmtnoprmfac1lem  44904  mod42tp1mod8  44942  stgoldbwt  45116  sbgoldbwt  45117  sbgoldbst  45118  evengpoap3  45139  wtgoldbnnsum4prm  45142  bgoldbnnsum3prm  45144  ply1mulgsumlem2  45616  ldepspr  45702  blennngt2o2  45826  inlinecirc02plem  46020