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  6402  funtp  6593  dmtpos  8237  frrlem11  8295  oaabs2  8661  ixpsnf1o  8952  fodomr  9142  fodomfir  9340  mapfienlem2  9418  cantnfrescl  9690  dfttrcl2  9738  cardprclem  9993  fin4en1  10323  ssfin4  10324  axdc3lem2  10465  axdc3lem4  10467  fpwwe2lem8  10652  recexsrlem  11117  nn0n0n1ge2b  12570  xmulpnf1  13290  ige2m2fzo  13744  swrdlsw  14685  swrd2lsw  14971  wrdl3s3  14981  lcmfass  16665  qredeu  16677  qnumdencoprm  16764  qeqnumdivden  16765  isacs1i  17669  subgga  19283  symgfixf1  19418  sylow1lem2  19580  sylow3lem1  19608  nn0gsumfz  19965  pzriprngALT  21456  evlsgsumadd  22049  evlsgsummul  22050  mhpmulcl  22087  mptcoe1fsupp  22151  evls1gsumadd  22262  evls1gsummul  22263  evl1gsummul  22298  mat1scmat  22477  smadiadetlem4  22607  mptcoe1matfsupp  22740  chfacfscmulgsum  22798  chfacfpmmulgsum  22802  topbas  22910  neips  23051  lmbrf  23198  rnelfm  23891  tsmsres  24082  reconnlem1  24766  lmmbrf  25214  iscauf  25232  caucfil  25235  cmetcaulem  25240  voliunlem1  25503  isosctrlem1  26780  bcmono  27240  2lgslem1a  27354  dchrvmasumlem2  27461  mulog2sumlem2  27498  pntlemb  27560  nodense  27656  conway  27763  etasslt  27777  slerec  27783  cofcutr  27884  precsexlem9  28169  usgr2pthlem  29745  2pthon3v  29925  elwspths2spth  29949  clwlkclwwlklem2fv2  29977  grpofo  30480  nvss  30574  nmosetn0  30746  hhsst  31247  pjoc1i  31412  chlejb1i  31457  cmbr4i  31582  pjjsi  31681  nmopun  31995  stlesi  32222  mdsl2bi  32304  mdslmd1lem1  32306  xraddge02  32734  supxrnemnf  32745  constrextdg2  33783  qtopt1  33866  lmxrge0  33983  esumcst  34094  sigagenval  34171  measdivcstALTV  34256  oms0  34329  ballotlemfc0  34525  ballotlemfcc  34526  bnj945  34804  bnj986  34986  bnj1421  35073  fv1stcnv  35794  fv2ndcnv  35795  fness  36367  nandsym1  36440  bj-finsumval0  37303  finixpnum  37629  poimirlem3  37647  poimirlem16  37660  poimirlem17  37661  poimirlem19  37663  poimirlem20  37664  poimirlem27  37671  ismblfin  37685  lcvexchlem5  39056  paddssat  39833  dibn0  41172  lclkrs2  41559  aks4d1p1p7  42087  eqresfnbd  42283  fiphp3d  42842  pellqrex  42902  jm2.16nn0  43028  onexlimgt  43267  cantnf2  43349  rp-fakeanorass  43537  clsk1indlem2  44066  icccncfext  45916  wallispilem4  46097  fmtnorec1  47551  fmtnoprmfac1lem  47578  mod42tp1mod8  47616  stgoldbwt  47790  sbgoldbwt  47791  sbgoldbst  47792  evengpoap3  47813  wtgoldbnnsum4prm  47816  bgoldbnnsum3prm  47818  isubgruhgr  47881  uhgrimisgrgric  47944  isubgr3stgrlem7  47984  gpgprismgr4cycl0  48105  ply1mulgsumlem2  48363  ldepspr  48449  blennngt2o2  48572  inlinecirc02plem  48766