Theorem jctir 530

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  jctr  534  ordunidif  6408  funtp  6591  dmtpos  8237  frrlem11  8296  oaabs2  8638  ixpsnf1o  8946  fodomr  9127  fodomfir  9298  mapfienlem2  9377  cantnfrescl  9656  dfttrcl2  9704  cardprclem  9985  fin4en1  10312  ssfin4  10313  axdc3lem2  10454  axdc3lem4  10456  fpwwe2lem8  10648  recexsrlem  11113  nn0n0n1ge2b  12598  xmulpnf1  13327  ige2m2fzo  13785  swrdlsw  14738  swrd2lsw  15026  wrdl3s3  15036  lcmfass  16737  qredeu  16749  qnumdencoprm  16837  qeqnumdivden  16838  isacs1i  17746  subgga  19428  symgfixf1  19565  sylow1lem2  19727  sylow3lem1  19755  nn0gsumfz  20112  pzriprngALT  21709  evlsgsumadd  22313  evlsgsummul  22314  mhpmulcl  22378  mptcoe1fsupp  22441  evls1gsumadd  22550  evls1gsummul  22551  evl1gsummul  22586  mat1scmat  22762  smadiadetlem4  22892  mptcoe1matfsupp  23028  chfacfscmulgsum  23086  chfacfpmmulgsum  23090  topbas  23198  neips  23339  lmbrf  23486  rnelfm  24180  tsmsres  24371  reconnlem1  25054  lmmbrf  25491  iscauf  25509  caucfil  25512  cmetcaulem  25517  voliunlem1  25779  isosctrlem1  27056  bcmono  27514  2lgslem1a  27628  dchrvmasumlem2  27735  mulog2sumlem2  27772  pntlemb  27834  nodense  27929  conway  28045  etaslts  28059  lesrec  28065  cofcutr  28190  precsexlem9  28481  usgr2pthlem  30229  2pthon3v  30412  elwspths2spth  30439  clwlkclwwlklem2fv2  30467  grpofo  30981  nvss  31075  nmosetn0  31247  hhsst  31748  pjoc1i  31913  chlejb1i  31958  cmbr4i  32083  pjjsi  32182  nmopun  32496  stlesi  32723  mdsl2bi  32805  mdslmd1lem1  32807  xraddge02  33229  supxrnemnf  33240  evlextv  34053  constrextdg2  34260  qtopt1  34346  lmxrge0  34463  esumcst  34574  sigagenval  34652  measdivcstALTV  34737  oms0  34809  ballotlemfc0  35005  ballotlemfcc  35006  bnj945  35284  bnj986  35465  bnj1421  35552  fv1stcnv  36357  fv2ndcnv  36358  fness  36969  nandsym1  37042  bj-finsumval0  38038  finixpnum  38360  poimirlem3  38373  poimirlem16  38386  poimirlem17  38387  poimirlem19  38389  poimirlem20  38390  poimirlem27  38397  ismblfin  38411  ecxrn2  39157  lcvexchlem5  39912  paddssat  40688  dibn0  42027  lclkrs2  42414  aks4d1p1p7  42941  eqresfnbd  43103  fiphp3d  43661  pellqrex  43721  jm2.16nn0  43846  onexlimgt  44085  cantnf2  44167  rp-fakeanorass  44354  clsk1indlem2  44883  icccncfext  46716  wallispilem4  46897  fmtnorec1  48441  fmtnoprmfac1lem  48468  mod42tp1mod8  48506  stgoldbwt  48693  sbgoldbwt  48694  sbgoldbst  48695  evengpoap3  48716  wtgoldbnnsum4prm  48719  bgoldbnnsum3prm  48721  isubgruhgr  48785  uhgrimisgrgric  48848  isubgr3stgrlem7  48889  gpgprismgr4cycl0  49023  ply1mulgsumlem2  49318  ldepspr  49404  blennngt2o2  49523  inlinecirc02plem  49717