Theorem jctir 528

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  jctr  532  ordunidif  6396  funtp  6578  dmtpos  8218  frrlem11  8277  oaabs2  8619  ixpsnf1o  8920  fodomr  9100  fodomfir  9272  mapfienlem2  9352  cantnfrescl  9631  dfttrcl2  9679  cardprclem  9937  fin4en1  10266  ssfin4  10267  axdc3lem2  10408  axdc3lem4  10410  fpwwe2lem8  10596  recexsrlem  11061  nn0n0n1ge2b  12550  xmulpnf1  13277  ige2m2fzo  13734  swrdlsw  14681  swrd2lsw  14965  wrdl3s3  14975  lcmfass  16680  qredeu  16692  qnumdencoprm  16780  qeqnumdivden  16781  isacs1i  17689  subgga  19340  symgfixf1  19477  sylow1lem2  19639  sylow3lem1  19667  nn0gsumfz  20024  pzriprngALT  21547  evlsgsumadd  22149  evlsgsummul  22150  mhpmulcl  22214  mptcoe1fsupp  22277  evls1gsumadd  22387  evls1gsummul  22388  evl1gsummul  22423  mat1scmat  22599  smadiadetlem4  22729  mptcoe1matfsupp  22862  chfacfscmulgsum  22920  chfacfpmmulgsum  22924  topbas  23032  neips  23173  lmbrf  23320  rnelfm  24013  tsmsres  24204  reconnlem1  24887  lmmbrf  25324  iscauf  25342  caucfil  25345  cmetcaulem  25350  voliunlem1  25612  isosctrlem1  26883  bcmono  27341  2lgslem1a  27455  dchrvmasumlem2  27562  mulog2sumlem2  27599  pntlemb  27661  nodense  27756  conway  27872  etaslts  27886  lesrec  27892  cofcutr  28017  precsexlem9  28308  usgr2pthlem  29963  2pthon3v  30143  elwspths2spth  30170  clwlkclwwlklem2fv2  30198  grpofo  30702  nvss  30796  nmosetn0  30968  hhsst  31469  pjoc1i  31634  chlejb1i  31679  cmbr4i  31804  pjjsi  31903  nmopun  32217  stlesi  32444  mdsl2bi  32526  mdslmd1lem1  32528  xraddge02  32959  supxrnemnf  32970  evlextv  33839  constrextdg2  34046  qtopt1  34132  lmxrge0  34249  esumcst  34360  sigagenval  34437  measdivcstALTV  34522  oms0  34594  ballotlemfc0  34790  ballotlemfcc  34791  bnj945  35069  bnj986  35250  bnj1421  35337  fv1stcnv  36127  fv2ndcnv  36128  fness  36709  nandsym1  36782  bj-finsumval0  37777  finixpnum  38104  poimirlem3  38122  poimirlem16  38135  poimirlem17  38136  poimirlem19  38138  poimirlem20  38139  poimirlem27  38146  ismblfin  38160  ecxrn2  38907  lcvexchlem5  39662  paddssat  40438  dibn0  41777  lclkrs2  42164  aks4d1p1p7  42691  eqresfnbd  42851  fiphp3d  43396  pellqrex  43456  jm2.16nn0  43581  onexlimgt  43820  cantnf2  43902  rp-fakeanorass  44089  clsk1indlem2  44618  icccncfext  46461  wallispilem4  46642  fmtnorec1  48146  fmtnoprmfac1lem  48173  mod42tp1mod8  48211  stgoldbwt  48398  sbgoldbwt  48399  sbgoldbst  48400  evengpoap3  48421  wtgoldbnnsum4prm  48424  bgoldbnnsum3prm  48426  isubgruhgr  48490  uhgrimisgrgric  48553  isubgr3stgrlem7  48594  gpgprismgr4cycl0  48728  ply1mulgsumlem2  49009  ldepspr  49095  blennngt2o2  49214  inlinecirc02plem  49408