Theorem jctir 519

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

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  jctr  523  ordunidif  6420  funtp  6611  dmtpos  8244  frrlem11  8302  oaabs2  8670  ixpsnf1o  8957  fodomr  9153  mapfienlem2  9431  cantnfrescl  9701  dfttrcl2  9749  cardprclem  10004  fin4en1  10334  ssfin4  10335  axdc3lem2  10476  axdc3lem4  10478  fpwwe2lem8  10663  recexsrlem  11128  nn0n0n1ge2b  12573  xmulpnf1  13288  ige2m2fzo  13730  swrdlsw  14653  swrd2lsw  14939  wrdl3s3  14949  lcmfass  16620  qredeu  16632  qnumdencoprm  16720  qeqnumdivden  16721  isacs1i  17640  subgga  19263  symgfixf1  19404  sylow1lem2  19566  sylow3lem1  19594  nn0gsumfz  19951  pzriprngALT  21438  evlsgsumadd  22059  evlsgsummul  22060  mhpmulcl  22096  mptcoe1fsupp  22158  evls1gsumadd  22268  evls1gsummul  22269  evl1gsummul  22304  mat1scmat  22485  smadiadetlem4  22615  mptcoe1matfsupp  22748  chfacfscmulgsum  22806  chfacfpmmulgsum  22810  topbas  22919  neips  23061  lmbrf  23208  rnelfm  23901  tsmsres  24092  reconnlem1  24786  lmmbrf  25234  iscauf  25252  caucfil  25255  cmetcaulem  25260  voliunlem1  25523  isosctrlem1  26795  bcmono  27255  2lgslem1a  27369  dchrvmasumlem2  27476  mulog2sumlem2  27513  pntlemb  27575  nodense  27671  conway  27778  etasslt  27792  slerec  27798  cofcutr  27890  precsexlem9  28163  usgr2pthlem  29649  2pthon3v  29826  elwspths2spth  29850  clwlkclwwlklem2fv2  29878  grpofo  30381  nvss  30475  nmosetn0  30647  hhsst  31148  pjoc1i  31313  chlejb1i  31358  cmbr4i  31483  pjjsi  31582  nmopun  31896  stlesi  32123  mdsl2bi  32205  mdslmd1lem1  32207  xraddge02  32608  supxrnemnf  32620  qtopt1  33567  lmxrge0  33684  esumcst  33813  sigagenval  33890  measdivcstALTV  33975  oms0  34048  ballotlemfc0  34243  ballotlemfcc  34244  bnj945  34535  bnj986  34717  bnj1421  34804  fv1stcnv  35503  fv2ndcnv  35504  fness  35964  nandsym1  36037  bj-finsumval0  36895  finixpnum  37209  poimirlem3  37227  poimirlem16  37240  poimirlem17  37241  poimirlem19  37243  poimirlem20  37244  poimirlem27  37251  ismblfin  37265  lcvexchlem5  38640  paddssat  39417  dibn0  40756  lclkrs2  41143  aks4d1p1p7  41677  eqresfnbd  41856  fiphp3d  42381  pellqrex  42441  jm2.16nn0  42567  onexlimgt  42813  cantnf2  42896  rp-fakeanorass  43085  clsk1indlem2  43614  icccncfext  45413  wallispilem4  45594  fmtnorec1  47014  fmtnoprmfac1lem  47041  mod42tp1mod8  47079  stgoldbwt  47253  sbgoldbwt  47254  sbgoldbst  47255  evengpoap3  47276  wtgoldbnnsum4prm  47279  bgoldbnnsum3prm  47281  isubgruhgr  47338  ply1mulgsumlem2  47641  ldepspr  47727  blennngt2o2  47851  inlinecirc02plem  48045