Theorem jctir 523

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

Syntax hints:   → wi 4   ∧ wa 398

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 399

This theorem is referenced by:  jctr  527  ordunidif  6238  funtp  6410  dmtpos  7903  oaabs2  8271  ixpsnf1o  8501  fodomr  8667  mapfienlem2  8868  cantnfrescl  9138  cardprclem  9407  fin4en1  9730  ssfin4  9731  axdc3lem2  9872  axdc3lem4  9874  fpwwe2lem9  10059  recexsrlem  10524  nn0n0n1ge2b  11962  xmulpnf1  12666  ige2m2fzo  13099  swrdlsw  14028  swrd2lsw  14313  wrdl3s3  14325  lcmfass  15989  qredeu  16001  qnumdencoprm  16084  qeqnumdivden  16085  isacs1i  16927  subgga  18429  symgfixf1  18564  sylow1lem2  18723  sylow3lem1  18751  nn0gsumfz  19103  evlsgsumadd  20303  evlsgsummul  20304  mptcoe1fsupp  20382  evls1gsumadd  20486  evls1gsummul  20487  evl1gsummul  20522  mat1scmat  21147  smadiadetlem4  21277  mptcoe1matfsupp  21409  chfacfscmulgsum  21467  chfacfpmmulgsum  21471  topbas  21579  neips  21720  lmbrf  21867  rnelfm  22560  tsmsres  22751  reconnlem1  23433  lmmbrf  23864  iscauf  23882  caucfil  23885  cmetcaulem  23890  voliunlem1  24150  isosctrlem1  25395  bcmono  25852  2lgslem1a  25966  dchrvmasumlem2  26073  mulog2sumlem2  26110  pntlemb  26172  usgr2pthlem  27543  2pthon3v  27721  elwspths2spth  27745  clwlkclwwlklem2fv2  27773  grpofo  28275  nvss  28369  nmosetn0  28541  hhsst  29042  pjoc1i  29207  chlejb1i  29252  cmbr4i  29377  pjjsi  29476  nmopun  29790  stlesi  30017  mdsl2bi  30099  mdslmd1lem1  30101  xraddge02  30479  supxrnemnf  30492  qtopt1  31099  lmxrge0  31195  esumcst  31322  sigagenval  31399  measdivcstALTV  31484  oms0  31555  ballotlemfc0  31750  ballotlemfcc  31751  bnj945  32045  bnj986  32227  bnj1421  32314  fv1stcnv  33020  fv2ndcnv  33021  dftrpred3g  33072  frrlem11  33133  nodense  33196  nulssgt  33263  conway  33264  etasslt  33274  slerec  33277  fness  33697  nandsym1  33770  bj-finsumval0  34566  finixpnum  34876  poimirlem3  34894  poimirlem16  34907  poimirlem17  34908  poimirlem19  34910  poimirlem20  34911  poimirlem27  34918  ismblfin  34932  lcvexchlem5  36173  paddssat  36949  dibn0  38288  lclkrs2  38675  fiphp3d  39414  pellqrex  39474  jm2.16nn0  39599  rp-fakeanorass  39877  clsk1indlem2  40390  icccncfext  42168  wallispilem4  42352  fmtnorec1  43698  fmtnoprmfac1lem  43725  mod42tp1mod8  43766  stgoldbwt  43940  sbgoldbwt  43941  sbgoldbst  43942  evengpoap3  43963  wtgoldbnnsum4prm  43966  bgoldbnnsum3prm  43968  ply1mulgsumlem2  44440  ldepspr  44527  blennngt2o2  44651  inlinecirc02plem  44772