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  6370  funtp  6557  dmtpos  8194  frrlem11  8252  oaabs2  8590  ixpsnf1o  8888  fodomr  9069  fodomfir  9255  mapfienlem2  9333  cantnfrescl  9605  dfttrcl2  9653  cardprclem  9908  fin4en1  10238  ssfin4  10239  axdc3lem2  10380  axdc3lem4  10382  fpwwe2lem8  10567  recexsrlem  11032  nn0n0n1ge2b  12487  xmulpnf1  13210  ige2m2fzo  13665  swrdlsw  14608  swrd2lsw  14894  wrdl3s3  14904  lcmfass  16592  qredeu  16604  qnumdencoprm  16691  qeqnumdivden  16692  isacs1i  17594  subgga  19208  symgfixf1  19343  sylow1lem2  19505  sylow3lem1  19533  nn0gsumfz  19890  pzriprngALT  21381  evlsgsumadd  21974  evlsgsummul  21975  mhpmulcl  22012  mptcoe1fsupp  22076  evls1gsumadd  22187  evls1gsummul  22188  evl1gsummul  22223  mat1scmat  22402  smadiadetlem4  22532  mptcoe1matfsupp  22665  chfacfscmulgsum  22723  chfacfpmmulgsum  22727  topbas  22835  neips  22976  lmbrf  23123  rnelfm  23816  tsmsres  24007  reconnlem1  24691  lmmbrf  25138  iscauf  25156  caucfil  25159  cmetcaulem  25164  voliunlem1  25427  isosctrlem1  26704  bcmono  27164  2lgslem1a  27278  dchrvmasumlem2  27385  mulog2sumlem2  27422  pntlemb  27484  nodense  27580  conway  27687  etasslt  27701  slerec  27707  cofcutr  27808  precsexlem9  28093  usgr2pthlem  29666  2pthon3v  29846  elwspths2spth  29870  clwlkclwwlklem2fv2  29898  grpofo  30401  nvss  30495  nmosetn0  30667  hhsst  31168  pjoc1i  31333  chlejb1i  31378  cmbr4i  31503  pjjsi  31602  nmopun  31916  stlesi  32143  mdsl2bi  32225  mdslmd1lem1  32227  xraddge02  32653  supxrnemnf  32664  constrextdg2  33712  qtopt1  33798  lmxrge0  33915  esumcst  34026  sigagenval  34103  measdivcstALTV  34188  oms0  34261  ballotlemfc0  34457  ballotlemfcc  34458  bnj945  34736  bnj986  34918  bnj1421  35005  fv1stcnv  35737  fv2ndcnv  35738  fness  36310  nandsym1  36383  bj-finsumval0  37246  finixpnum  37572  poimirlem3  37590  poimirlem16  37603  poimirlem17  37604  poimirlem19  37606  poimirlem20  37607  poimirlem27  37614  ismblfin  37628  lcvexchlem5  39004  paddssat  39781  dibn0  41120  lclkrs2  41507  aks4d1p1p7  42035  eqresfnbd  42193  fiphp3d  42780  pellqrex  42840  jm2.16nn0  42966  onexlimgt  43205  cantnf2  43287  rp-fakeanorass  43475  clsk1indlem2  44004  icccncfext  45858  wallispilem4  46039  fmtnorec1  47511  fmtnoprmfac1lem  47538  mod42tp1mod8  47576  stgoldbwt  47750  sbgoldbwt  47751  sbgoldbst  47752  evengpoap3  47773  wtgoldbnnsum4prm  47776  bgoldbnnsum3prm  47778  isubgruhgr  47841  uhgrimisgrgric  47904  isubgr3stgrlem7  47944  gpgprismgr4cycl0  48069  ply1mulgsumlem2  48349  ldepspr  48435  blennngt2o2  48554  inlinecirc02plem  48748