Theorem jctir 520

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  jctr  524  ordunidif  6433  funtp  6623  dmtpos  8263  frrlem11  8321  oaabs2  8687  ixpsnf1o  8978  fodomr  9168  fodomfir  9368  mapfienlem2  9446  cantnfrescl  9716  dfttrcl2  9764  cardprclem  10019  fin4en1  10349  ssfin4  10350  axdc3lem2  10491  axdc3lem4  10493  fpwwe2lem8  10678  recexsrlem  11143  nn0n0n1ge2b  12595  xmulpnf1  13316  ige2m2fzo  13767  swrdlsw  14705  swrd2lsw  14991  wrdl3s3  15001  lcmfass  16683  qredeu  16695  qnumdencoprm  16782  qeqnumdivden  16783  isacs1i  17700  subgga  19318  symgfixf1  19455  sylow1lem2  19617  sylow3lem1  19645  nn0gsumfz  20002  pzriprngALT  21506  evlsgsumadd  22115  evlsgsummul  22116  mhpmulcl  22153  mptcoe1fsupp  22217  evls1gsumadd  22328  evls1gsummul  22329  evl1gsummul  22364  mat1scmat  22545  smadiadetlem4  22675  mptcoe1matfsupp  22808  chfacfscmulgsum  22866  chfacfpmmulgsum  22870  topbas  22979  neips  23121  lmbrf  23268  rnelfm  23961  tsmsres  24152  reconnlem1  24848  lmmbrf  25296  iscauf  25314  caucfil  25317  cmetcaulem  25322  voliunlem1  25585  isosctrlem1  26861  bcmono  27321  2lgslem1a  27435  dchrvmasumlem2  27542  mulog2sumlem2  27579  pntlemb  27641  nodense  27737  conway  27844  etasslt  27858  slerec  27864  cofcutr  27958  precsexlem9  28239  usgr2pthlem  29783  2pthon3v  29963  elwspths2spth  29987  clwlkclwwlklem2fv2  30015  grpofo  30518  nvss  30612  nmosetn0  30784  hhsst  31285  pjoc1i  31450  chlejb1i  31495  cmbr4i  31620  pjjsi  31719  nmopun  32033  stlesi  32260  mdsl2bi  32342  mdslmd1lem1  32344  xraddge02  32760  supxrnemnf  32772  constrextdg2  33790  qtopt1  33834  lmxrge0  33951  esumcst  34064  sigagenval  34141  measdivcstALTV  34226  oms0  34299  ballotlemfc0  34495  ballotlemfcc  34496  bnj945  34787  bnj986  34969  bnj1421  35056  fv1stcnv  35777  fv2ndcnv  35778  fness  36350  nandsym1  36423  bj-finsumval0  37286  finixpnum  37612  poimirlem3  37630  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  poimirlem27  37654  ismblfin  37668  lcvexchlem5  39039  paddssat  39816  dibn0  41155  lclkrs2  41542  aks4d1p1p7  42075  eqresfnbd  42273  fiphp3d  42830  pellqrex  42890  jm2.16nn0  43016  onexlimgt  43255  cantnf2  43338  rp-fakeanorass  43526  clsk1indlem2  44055  icccncfext  45902  wallispilem4  46083  fmtnorec1  47524  fmtnoprmfac1lem  47551  mod42tp1mod8  47589  stgoldbwt  47763  sbgoldbwt  47764  sbgoldbst  47765  evengpoap3  47786  wtgoldbnnsum4prm  47789  bgoldbnnsum3prm  47791  isubgruhgr  47854  uhgrimisgrgric  47899  isubgr3stgrlem7  47939  ply1mulgsumlem2  48304  ldepspr  48390  blennngt2o2  48513  inlinecirc02plem  48707