Theorem jctir 559

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  jctr  563  uniintsn  4449  ordunidif  5690  funtp  5859  foimacnv  6067  respreima  6252  fpr  6326  curry1  7156  dmtpos  7251  wfrlem13  7314  tfrlem10  7370  oawordeulem  7521  oelim2  7562  oaabs2  7612  ixpsnf1o  7834  ssdomg  7887  fodomr  7996  limenpsi  8020  cantnfrescl  8456  cardprclem  8688  fin4en1  9014  ssfin4  9015  axdc3lem2  9156  axdc3lem4  9158  fpwwe2lem9  9339  gruina  9519  reclem2pr  9749  recexsrlem  9803  nn0n0n1ge2b  11236  xmulpnf1  11976  ige2m2fzo  12398  swrdlsw  13304  swrd2lsw  13543  wrdl3s3  13553  climeu  14134  odd2np1  14903  algcvgblem  15128  lcmfass  15197  qredeu  15210  qnumdencoprm  15291  qeqnumdivden  15292  isacs1i  16141  subgga  17556  symgfixf1  17680  sylow1lem2  17837  sylow3lem1  17865  nn0gsumfz  18203  mptcoe1fsupp  19406  evls1gsumadd  19510  evls1gsummul  19511  evl1gsummul  19545  mat1scmat  20164  smadiadetlem4  20294  mptcoe1matfsupp  20426  chfacfscmulgsum  20484  chfacfpmmulgsum  20488  eltg3i  20576  topbas  20587  neips  20727  restntr  20796  lmbrf  20874  cmpcld  21015  rnelfm  21567  tsmsres  21757  reconnlem1  22437  lmmbrf  22868  iscauf  22886  caucfil  22889  cmetcaulem  22894  ovolctb2  23067  voliunlem1  23125  isosctrlem1  24348  bcmono  24802  2lgslem1a  24916  dchrvmasumlem2  24987  mulog2sumlem2  25024  pntlemb  25086  axlowdimlem13  25634  2pthon3v  26134  wlkdvspthlem  26137  constr3cycl  26189  0clwlk  26293  clwlkisclwwlklem2fv2  26311  clwlkf1clwwlk  26377  frghash2spot  26590  extwwlkfablem2  26605  numclwwlk6  26640  grpofo  26737  nvss  26832  nmosetn0  27004  hhsst  27507  pjoc1i  27674  chlejb1i  27719  cmbr4i  27844  pjjsi  27943  nmopun  28257  stlesi  28484  mdsl2bi  28566  mdslmd1lem1  28568  xraddge02  28911  supxrnemnf  28924  qtopt1  29230  lmxrge0  29326  esumcst  29452  sigagenval  29530  measdivcstOLD  29614  oms0  29686  ballotlemfc0  29881  ballotlemfcc  29882  bnj945  30098  bnj150  30200  bnj986  30278  bnj1421  30364  dftrpred3g  30977  nodense  31088  nobndup  31099  fness  31514  nandsym1  31591  bj-finsumval0  32324  finixpnum  32564  poimirlem3  32582  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  poimirlem27  32606  mblfinlem3  32618  ismblfin  32620  rngoideu  32872  lcvexchlem5  33343  paddssat  34118  dibn0  35460  lclkrs2  35847  fiphp3d  36401  pellqrex  36461  jm2.16nn0  36589  rp-fakeanorass  36877  clsk1indlem2  37360  rfcnpre1  38201  icccncfext  38773  wallispilem4  38961  fmtnorec1  39987  fmtnoprmfac1lem  40014  mod42tp1mod8  40057  stgoldbwt  40198  bgoldbwt  40199  bgoldbst  40200  evengpoap3  40215  wtgoldbnnsum4prm  40218  bgoldbnnsum3prm  40220  usgr2pthlem  40969  2pthon3v-av  41150  elwspths2spth  41171  clwlkclwwlklem2fv2  41205  clwlksf1clwwlk  41276  frgrhash2wsp  41497  ply1mulgsumlem2  41969  ldepspr  42056  blennngt2o2  42184