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  6357  funtp  6539  dmtpos  8171  frrlem11  8229  oaabs2  8567  ixpsnf1o  8865  fodomr  9045  fodomfir  9218  mapfienlem2  9296  cantnfrescl  9572  dfttrcl2  9620  cardprclem  9875  fin4en1  10203  ssfin4  10204  axdc3lem2  10345  axdc3lem4  10347  fpwwe2lem8  10532  recexsrlem  10997  nn0n0n1ge2b  12453  xmulpnf1  13176  ige2m2fzo  13631  swrdlsw  14574  swrd2lsw  14859  wrdl3s3  14869  lcmfass  16557  qredeu  16569  qnumdencoprm  16656  qeqnumdivden  16657  isacs1i  17563  subgga  19179  symgfixf1  19316  sylow1lem2  19478  sylow3lem1  19506  nn0gsumfz  19863  pzriprngALT  21402  evlsgsumadd  21996  evlsgsummul  21997  mhpmulcl  22034  mptcoe1fsupp  22098  evls1gsumadd  22209  evls1gsummul  22210  evl1gsummul  22245  mat1scmat  22424  smadiadetlem4  22554  mptcoe1matfsupp  22687  chfacfscmulgsum  22745  chfacfpmmulgsum  22749  topbas  22857  neips  22998  lmbrf  23145  rnelfm  23838  tsmsres  24029  reconnlem1  24713  lmmbrf  25160  iscauf  25178  caucfil  25181  cmetcaulem  25186  voliunlem1  25449  isosctrlem1  26726  bcmono  27186  2lgslem1a  27300  dchrvmasumlem2  27407  mulog2sumlem2  27444  pntlemb  27506  nodense  27602  conway  27710  etasslt  27724  slerec  27730  cofcutr  27837  precsexlem9  28122  usgr2pthlem  29708  2pthon3v  29888  elwspths2spth  29912  clwlkclwwlklem2fv2  29940  grpofo  30443  nvss  30537  nmosetn0  30709  hhsst  31210  pjoc1i  31375  chlejb1i  31420  cmbr4i  31545  pjjsi  31644  nmopun  31958  stlesi  32185  mdsl2bi  32267  mdslmd1lem1  32269  xraddge02  32700  supxrnemnf  32711  constrextdg2  33716  qtopt1  33802  lmxrge0  33919  esumcst  34030  sigagenval  34107  measdivcstALTV  34192  oms0  34265  ballotlemfc0  34461  ballotlemfcc  34462  bnj945  34740  bnj986  34922  bnj1421  35009  fv1stcnv  35754  fv2ndcnv  35755  fness  36327  nandsym1  36400  bj-finsumval0  37263  finixpnum  37589  poimirlem3  37607  poimirlem16  37620  poimirlem17  37621  poimirlem19  37623  poimirlem20  37624  poimirlem27  37631  ismblfin  37645  lcvexchlem5  39021  paddssat  39797  dibn0  41136  lclkrs2  41523  aks4d1p1p7  42051  eqresfnbd  42209  fiphp3d  42796  pellqrex  42856  jm2.16nn0  42981  onexlimgt  43220  cantnf2  43302  rp-fakeanorass  43490  clsk1indlem2  44019  icccncfext  45872  wallispilem4  46053  fmtnorec1  47525  fmtnoprmfac1lem  47552  mod42tp1mod8  47590  stgoldbwt  47764  sbgoldbwt  47765  sbgoldbst  47766  evengpoap3  47787  wtgoldbnnsum4prm  47790  bgoldbnnsum3prm  47792  isubgruhgr  47856  uhgrimisgrgric  47919  isubgr3stgrlem7  47960  gpgprismgr4cycl0  48094  ply1mulgsumlem2  48376  ldepspr  48462  blennngt2o2  48581  inlinecirc02plem  48775