Theorem jctir 521

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  jctr  525  ordunidif  6318  funtp  6498  dmtpos  8063  frrlem11  8121  oaabs2  8488  ixpsnf1o  8735  fodomr  8924  mapfienlem2  9174  cantnfrescl  9443  dfttrcl2  9491  cardprclem  9746  fin4en1  10074  ssfin4  10075  axdc3lem2  10216  axdc3lem4  10218  fpwwe2lem8  10403  recexsrlem  10868  nn0n0n1ge2b  12310  xmulpnf1  13017  ige2m2fzo  13459  swrdlsw  14389  swrd2lsw  14674  wrdl3s3  14686  lcmfass  16360  qredeu  16372  qnumdencoprm  16458  qeqnumdivden  16459  isacs1i  17375  subgga  18915  symgfixf1  19054  sylow1lem2  19213  sylow3lem1  19241  nn0gsumfz  19594  evlsgsumadd  21310  evlsgsummul  21311  mhpmulcl  21348  mptcoe1fsupp  21395  evls1gsumadd  21499  evls1gsummul  21500  evl1gsummul  21535  mat1scmat  21697  smadiadetlem4  21827  mptcoe1matfsupp  21960  chfacfscmulgsum  22018  chfacfpmmulgsum  22022  topbas  22131  neips  22273  lmbrf  22420  rnelfm  23113  tsmsres  23304  reconnlem1  23998  lmmbrf  24435  iscauf  24453  caucfil  24456  cmetcaulem  24461  voliunlem1  24723  isosctrlem1  25977  bcmono  26434  2lgslem1a  26548  dchrvmasumlem2  26655  mulog2sumlem2  26692  pntlemb  26754  usgr2pthlem  28140  2pthon3v  28317  elwspths2spth  28341  clwlkclwwlklem2fv2  28369  grpofo  28870  nvss  28964  nmosetn0  29136  hhsst  29637  pjoc1i  29802  chlejb1i  29847  cmbr4i  29972  pjjsi  30071  nmopun  30385  stlesi  30612  mdsl2bi  30694  mdslmd1lem1  30696  xraddge02  31088  supxrnemnf  31100  qtopt1  31794  lmxrge0  31911  esumcst  32040  sigagenval  32117  measdivcstALTV  32202  oms0  32273  ballotlemfc0  32468  ballotlemfcc  32469  bnj945  32762  bnj986  32944  bnj1421  33031  fv1stcnv  33760  fv2ndcnv  33761  nodense  33904  conway  34002  etasslt  34016  slerec  34022  cofcutr  34101  fness  34547  nandsym1  34620  bj-finsumval0  35465  finixpnum  35771  poimirlem3  35789  poimirlem16  35802  poimirlem17  35803  poimirlem19  35805  poimirlem20  35806  poimirlem27  35813  ismblfin  35827  lcvexchlem5  37059  paddssat  37835  dibn0  39174  lclkrs2  39561  aks4d1p1p7  40089  fiphp3d  40648  pellqrex  40708  jm2.16nn0  40833  rp-fakeanorass  41127  clsk1indlem2  41659  icccncfext  43435  wallispilem4  43616  fmtnorec1  45000  fmtnoprmfac1lem  45027  mod42tp1mod8  45065  stgoldbwt  45239  sbgoldbwt  45240  sbgoldbst  45241  evengpoap3  45262  wtgoldbnnsum4prm  45265  bgoldbnnsum3prm  45267  ply1mulgsumlem2  45739  ldepspr  45825  blennngt2o2  45949  inlinecirc02plem  46143