Theorem jctir 522

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  jctr  526  ordunidif  6414  funtp  6606  dmtpos  8223  frrlem11  8281  oaabs2  8648  ixpsnf1o  8932  fodomr  9128  mapfienlem2  9401  cantnfrescl  9671  dfttrcl2  9719  cardprclem  9974  fin4en1  10304  ssfin4  10305  axdc3lem2  10446  axdc3lem4  10448  fpwwe2lem8  10633  recexsrlem  11098  nn0n0n1ge2b  12540  xmulpnf1  13253  ige2m2fzo  13695  swrdlsw  14617  swrd2lsw  14903  wrdl3s3  14913  lcmfass  16583  qredeu  16595  qnumdencoprm  16681  qeqnumdivden  16682  isacs1i  17601  subgga  19164  symgfixf1  19305  sylow1lem2  19467  sylow3lem1  19495  nn0gsumfz  19852  evlsgsumadd  21654  evlsgsummul  21655  mhpmulcl  21692  mptcoe1fsupp  21739  evls1gsumadd  21843  evls1gsummul  21844  evl1gsummul  21879  mat1scmat  22041  smadiadetlem4  22171  mptcoe1matfsupp  22304  chfacfscmulgsum  22362  chfacfpmmulgsum  22366  topbas  22475  neips  22617  lmbrf  22764  rnelfm  23457  tsmsres  23648  reconnlem1  24342  lmmbrf  24779  iscauf  24797  caucfil  24800  cmetcaulem  24805  voliunlem1  25067  isosctrlem1  26323  bcmono  26780  2lgslem1a  26894  dchrvmasumlem2  27001  mulog2sumlem2  27038  pntlemb  27100  nodense  27195  conway  27300  etasslt  27314  slerec  27320  cofcutr  27411  precsexlem9  27661  usgr2pthlem  29020  2pthon3v  29197  elwspths2spth  29221  clwlkclwwlklem2fv2  29249  grpofo  29752  nvss  29846  nmosetn0  30018  hhsst  30519  pjoc1i  30684  chlejb1i  30729  cmbr4i  30854  pjjsi  30953  nmopun  31267  stlesi  31494  mdsl2bi  31576  mdslmd1lem1  31578  xraddge02  31969  supxrnemnf  31981  qtopt1  32815  lmxrge0  32932  esumcst  33061  sigagenval  33138  measdivcstALTV  33223  oms0  33296  ballotlemfc0  33491  ballotlemfcc  33492  bnj945  33784  bnj986  33966  bnj1421  34053  fv1stcnv  34748  fv2ndcnv  34749  fness  35234  nandsym1  35307  bj-finsumval0  36166  finixpnum  36473  poimirlem3  36491  poimirlem16  36504  poimirlem17  36505  poimirlem19  36507  poimirlem20  36508  poimirlem27  36515  ismblfin  36529  lcvexchlem5  37908  paddssat  38685  dibn0  40024  lclkrs2  40411  aks4d1p1p7  40939  eqresfnbd  41054  fiphp3d  41557  pellqrex  41617  jm2.16nn0  41743  onexlimgt  41992  cantnf2  42075  rp-fakeanorass  42264  clsk1indlem2  42793  icccncfext  44603  wallispilem4  44784  fmtnorec1  46205  fmtnoprmfac1lem  46232  mod42tp1mod8  46270  stgoldbwt  46444  sbgoldbwt  46445  sbgoldbst  46446  evengpoap3  46467  wtgoldbnnsum4prm  46470  bgoldbnnsum3prm  46472  pzriprngALT  46819  ply1mulgsumlem2  47068  ldepspr  47154  blennngt2o2  47278  inlinecirc02plem  47472