Theorem jctir 529

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  jctr  533  ordunidif  6411  funtp  6593  dmtpos  8230  frrlem11  8289  oaabs2  8631  ixpsnf1o  8932  fodomr  9112  fodomfir  9283  mapfienlem2  9362  cantnfrescl  9641  dfttrcl2  9689  cardprclem  9961  fin4en1  10288  ssfin4  10289  axdc3lem2  10430  axdc3lem4  10432  fpwwe2lem8  10618  recexsrlem  11083  nn0n0n1ge2b  12568  xmulpnf1  13295  ige2m2fzo  13753  swrdlsw  14701  swrd2lsw  14985  wrdl3s3  14995  lcmfass  16699  qredeu  16711  qnumdencoprm  16799  qeqnumdivden  16800  isacs1i  17708  subgga  19365  symgfixf1  19502  sylow1lem2  19664  sylow3lem1  19692  nn0gsumfz  20049  pzriprngALT  21645  evlsgsumadd  22247  evlsgsummul  22248  mhpmulcl  22312  mptcoe1fsupp  22375  evls1gsumadd  22484  evls1gsummul  22485  evl1gsummul  22520  mat1scmat  22696  smadiadetlem4  22826  mptcoe1matfsupp  22959  chfacfscmulgsum  23017  chfacfpmmulgsum  23021  topbas  23129  neips  23270  lmbrf  23417  rnelfm  24110  tsmsres  24301  reconnlem1  24984  lmmbrf  25421  iscauf  25439  caucfil  25442  cmetcaulem  25447  voliunlem1  25709  isosctrlem1  26983  bcmono  27441  2lgslem1a  27555  dchrvmasumlem2  27662  mulog2sumlem2  27699  pntlemb  27761  nodense  27856  conway  27972  etaslts  27986  lesrec  27992  cofcutr  28117  precsexlem9  28408  usgr2pthlem  30112  2pthon3v  30292  elwspths2spth  30319  clwlkclwwlklem2fv2  30347  grpofo  30851  nvss  30945  nmosetn0  31117  hhsst  31618  pjoc1i  31783  chlejb1i  31828  cmbr4i  31953  pjjsi  32052  nmopun  32366  stlesi  32593  mdsl2bi  32675  mdslmd1lem1  32677  xraddge02  33102  supxrnemnf  33113  evlextv  33932  constrextdg2  34139  qtopt1  34225  lmxrge0  34342  esumcst  34453  sigagenval  34530  measdivcstALTV  34615  oms0  34687  ballotlemfc0  34883  ballotlemfcc  34884  bnj945  35162  bnj986  35343  bnj1421  35430  fv1stcnv  36269  fv2ndcnv  36270  fness  36860  nandsym1  36933  bj-finsumval0  37929  finixpnum  38256  poimirlem3  38274  poimirlem16  38287  poimirlem17  38288  poimirlem19  38290  poimirlem20  38291  poimirlem27  38298  ismblfin  38312  ecxrn2  39057  lcvexchlem5  39812  paddssat  40588  dibn0  41927  lclkrs2  42314  aks4d1p1p7  42841  eqresfnbd  43003  fiphp3d  43546  pellqrex  43606  jm2.16nn0  43731  onexlimgt  43970  cantnf2  44052  rp-fakeanorass  44239  clsk1indlem2  44768  icccncfext  46601  wallispilem4  46782  fmtnorec1  48289  fmtnoprmfac1lem  48316  mod42tp1mod8  48354  stgoldbwt  48541  sbgoldbwt  48542  sbgoldbst  48543  evengpoap3  48564  wtgoldbnnsum4prm  48567  bgoldbnnsum3prm  48569  isubgruhgr  48633  uhgrimisgrgric  48696  isubgr3stgrlem7  48737  gpgprismgr4cycl0  48871  ply1mulgsumlem2  49167  ldepspr  49253  blennngt2o2  49372  inlinecirc02plem  49566