Theorem jctir 521

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 512	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 206  df-an 397

This theorem is referenced by:  jctr  525  ordunidif  6334  funtp  6525  dmtpos  8099  frrlem11  8157  oaabs2  8525  ixpsnf1o  8772  fodomr  8968  mapfienlem2  9233  cantnfrescl  9502  dfttrcl2  9550  cardprclem  9805  fin4en1  10135  ssfin4  10136  axdc3lem2  10277  axdc3lem4  10279  fpwwe2lem8  10464  recexsrlem  10929  nn0n0n1ge2b  12371  xmulpnf1  13078  ige2m2fzo  13520  swrdlsw  14449  swrd2lsw  14734  wrdl3s3  14746  lcmfass  16418  qredeu  16430  qnumdencoprm  16516  qeqnumdivden  16517  isacs1i  17433  subgga  18973  symgfixf1  19112  sylow1lem2  19271  sylow3lem1  19299  nn0gsumfz  19652  evlsgsumadd  21372  evlsgsummul  21373  mhpmulcl  21410  mptcoe1fsupp  21457  evls1gsumadd  21561  evls1gsummul  21562  evl1gsummul  21597  mat1scmat  21759  smadiadetlem4  21889  mptcoe1matfsupp  22022  chfacfscmulgsum  22080  chfacfpmmulgsum  22084  topbas  22193  neips  22335  lmbrf  22482  rnelfm  23175  tsmsres  23366  reconnlem1  24060  lmmbrf  24497  iscauf  24515  caucfil  24518  cmetcaulem  24523  voliunlem1  24785  isosctrlem1  26039  bcmono  26496  2lgslem1a  26610  dchrvmasumlem2  26717  mulog2sumlem2  26754  pntlemb  26816  usgr2pthlem  28239  2pthon3v  28416  elwspths2spth  28440  clwlkclwwlklem2fv2  28468  grpofo  28969  nvss  29063  nmosetn0  29235  hhsst  29736  pjoc1i  29901  chlejb1i  29946  cmbr4i  30071  pjjsi  30170  nmopun  30484  stlesi  30711  mdsl2bi  30793  mdslmd1lem1  30795  xraddge02  31187  supxrnemnf  31199  qtopt1  31891  lmxrge0  32008  esumcst  32137  sigagenval  32214  measdivcstALTV  32299  oms0  32370  ballotlemfc0  32565  ballotlemfcc  32566  bnj945  32859  bnj986  33041  bnj1421  33128  fv1stcnv  33853  fv2ndcnv  33854  nodense  33956  conway  34054  etasslt  34068  slerec  34074  cofcutr  34153  fness  34599  nandsym1  34672  bj-finsumval0  35516  finixpnum  35822  poimirlem3  35840  poimirlem16  35853  poimirlem17  35854  poimirlem19  35856  poimirlem20  35857  poimirlem27  35864  ismblfin  35878  lcvexchlem5  37264  paddssat  38040  dibn0  39379  lclkrs2  39766  aks4d1p1p7  40294  fiphp3d  40851  pellqrex  40911  jm2.16nn0  41037  rp-fakeanorass  41348  clsk1indlem2  41880  icccncfext  43672  wallispilem4  43853  fmtnorec1  45248  fmtnoprmfac1lem  45275  mod42tp1mod8  45313  stgoldbwt  45487  sbgoldbwt  45488  sbgoldbst  45489  evengpoap3  45510  wtgoldbnnsum4prm  45513  bgoldbnnsum3prm  45515  ply1mulgsumlem2  45987  ldepspr  46073  blennngt2o2  46197  inlinecirc02plem  46391