Theorem jctir 538

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 532	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  jctr  542  uniintsn  4324  ordunidif  4931  funtp  5645  foimacnv  5838  respreima  6016  fpr  6079  curry1  6892  dmtpos  6986  tfrlem10  7075  oawordeulem  7222  oelim2  7263  oaabs2  7313  ixpsnf1o  7529  ssdomg  7581  fodomr  7688  limenpsi  7712  cantnfrescl  8116  cardprclem  8381  fin4en1  8710  ssfin4  8711  axdc3lem2  8852  axdc3lem4  8854  fpwwe2lem9  9037  gruina  9217  reclem2pr  9447  recexsrlem  9501  nn0n0n1ge2b  10885  xmulpnf1  11495  ige2m2fzo  11879  swrdlsw  12677  swrd2lsw  12890  climeu  13378  odd2np1  14046  algcvgblem  14206  qredeu  14248  qnumdencoprm  14278  qeqnumdivden  14279  isacs1i  15054  subgga  16338  symgfixf1  16462  sylow1lem2  16619  sylow3lem1  16647  nn0gsumfz  17012  mptcoe1fsupp  18255  evls1gsumadd  18361  evls1gsummul  18362  evl1gsummul  18396  mat1scmat  19041  smadiadetlem4  19171  mptcoe1matfsupp  19303  chfacfscmulgsum  19361  chfacfpmmulgsum  19365  eltg3i  19462  topbas  19474  neips  19614  restntr  19683  lmbrf  19761  cmpcld  19902  rnelfm  20454  tsmsres  20646  reconnlem1  21331  lmmbrf  21701  iscauf  21719  caucfil  21722  cmetcaulem  21727  ovolctb2  21903  voliunlem1  21960  isosctrlem1  23152  bcmono  23552  dchrvmasumlem2  23683  mulog2sumlem2  23720  pntlemb  23782  axlowdimlem13  24257  2pthon3v  24606  wlkdvspthlem  24609  constr3cycl  24661  0clwlk  24765  clwlkisclwwlklem2fv2  24783  clwlkf1clwwlk  24850  clwlksizeeq  24852  frghash2spot  25063  extwwlkfablem2  25078  numclwwlk6  25113  grpofo  25201  rngoideu  25386  nvss  25486  nmosetn0  25680  hhsst  26182  pjoc1i  26349  chlejb1i  26394  cmbr4i  26519  pjjsi  26618  nmopun  26933  stlesi  27160  mdsl2bi  27242  mdslmd1lem1  27244  xraddge02  27577  supxrnemnf  27583  qtopt1  27838  lmxrge0  27934  esumcst  28071  sigagenval  28140  measdivcstOLD  28195  ballotlemfc0  28431  ballotlemfcc  28432  relexpsucr  29053  dftrpred3g  29316  wfrlem13  29355  nodense  29449  nobndup  29460  nandsym1  29887  finixpnum  30038  mblfinlem3  30053  ismblfin  30055  fness  30167  fiphp3d  30753  pellqrex  30815  jm2.16nn0  30946  rfcnpre1  31394  icccncfext  31690  wallispilem4  31850  usgra2pthlem1  32353  ply1mulgsumlem2  32987  ldepspr  33074  bnj945  33832  bnj150  33934  bnj986  34012  bnj1421  34098  bj-finsumval0  34663  lcvexchlem5  34763  paddssat  35538  dibn0  36880  lclkrs2  37267  rp-fakeanorass  37737

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 185  df-an 371