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  6382  funtp  6573  dmtpos  8217  frrlem11  8275  oaabs2  8613  ixpsnf1o  8911  fodomr  9092  fodomfir  9279  mapfienlem2  9357  cantnfrescl  9629  dfttrcl2  9677  cardprclem  9932  fin4en1  10262  ssfin4  10263  axdc3lem2  10404  axdc3lem4  10406  fpwwe2lem8  10591  recexsrlem  11056  nn0n0n1ge2b  12511  xmulpnf1  13234  ige2m2fzo  13689  swrdlsw  14632  swrd2lsw  14918  wrdl3s3  14928  lcmfass  16616  qredeu  16628  qnumdencoprm  16715  qeqnumdivden  16716  isacs1i  17618  subgga  19232  symgfixf1  19367  sylow1lem2  19529  sylow3lem1  19557  nn0gsumfz  19914  pzriprngALT  21405  evlsgsumadd  21998  evlsgsummul  21999  mhpmulcl  22036  mptcoe1fsupp  22100  evls1gsumadd  22211  evls1gsummul  22212  evl1gsummul  22247  mat1scmat  22426  smadiadetlem4  22556  mptcoe1matfsupp  22689  chfacfscmulgsum  22747  chfacfpmmulgsum  22751  topbas  22859  neips  23000  lmbrf  23147  rnelfm  23840  tsmsres  24031  reconnlem1  24715  lmmbrf  25162  iscauf  25180  caucfil  25183  cmetcaulem  25188  voliunlem1  25451  isosctrlem1  26728  bcmono  27188  2lgslem1a  27302  dchrvmasumlem2  27409  mulog2sumlem2  27446  pntlemb  27508  nodense  27604  conway  27711  etasslt  27725  slerec  27731  cofcutr  27832  precsexlem9  28117  usgr2pthlem  29693  2pthon3v  29873  elwspths2spth  29897  clwlkclwwlklem2fv2  29925  grpofo  30428  nvss  30522  nmosetn0  30694  hhsst  31195  pjoc1i  31360  chlejb1i  31405  cmbr4i  31530  pjjsi  31629  nmopun  31943  stlesi  32170  mdsl2bi  32252  mdslmd1lem1  32254  xraddge02  32680  supxrnemnf  32691  constrextdg2  33739  qtopt1  33825  lmxrge0  33942  esumcst  34053  sigagenval  34130  measdivcstALTV  34215  oms0  34288  ballotlemfc0  34484  ballotlemfcc  34485  bnj945  34763  bnj986  34945  bnj1421  35032  fv1stcnv  35764  fv2ndcnv  35765  fness  36337  nandsym1  36410  bj-finsumval0  37273  finixpnum  37599  poimirlem3  37617  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem27  37641  ismblfin  37655  lcvexchlem5  39031  paddssat  39808  dibn0  41147  lclkrs2  41534  aks4d1p1p7  42062  eqresfnbd  42220  fiphp3d  42807  pellqrex  42867  jm2.16nn0  42993  onexlimgt  43232  cantnf2  43314  rp-fakeanorass  43502  clsk1indlem2  44031  icccncfext  45885  wallispilem4  46066  fmtnorec1  47538  fmtnoprmfac1lem  47565  mod42tp1mod8  47603  stgoldbwt  47777  sbgoldbwt  47778  sbgoldbst  47779  evengpoap3  47800  wtgoldbnnsum4prm  47803  bgoldbnnsum3prm  47805  isubgruhgr  47868  uhgrimisgrgric  47931  isubgr3stgrlem7  47971  gpgprismgr4cycl0  48096  ply1mulgsumlem2  48376  ldepspr  48462  blennngt2o2  48581  inlinecirc02plem  48775