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  6373  funtp  6555  dmtpos  8188  frrlem11  8246  oaabs2  8585  ixpsnf1o  8886  fodomr  9066  fodomfir  9238  mapfienlem2  9319  cantnfrescl  9597  dfttrcl2  9645  cardprclem  9903  fin4en1  10231  ssfin4  10232  axdc3lem2  10373  axdc3lem4  10375  fpwwe2lem8  10561  recexsrlem  11026  nn0n0n1ge2b  12506  xmulpnf1  13226  ige2m2fzo  13683  swrdlsw  14630  swrd2lsw  14914  wrdl3s3  14924  lcmfass  16615  qredeu  16627  qnumdencoprm  16715  qeqnumdivden  16716  isacs1i  17623  subgga  19275  symgfixf1  19412  sylow1lem2  19574  sylow3lem1  19602  nn0gsumfz  19959  pzriprngALT  21475  evlsgsumadd  22074  evlsgsummul  22075  mhpmulcl  22115  mptcoe1fsupp  22179  evls1gsumadd  22289  evls1gsummul  22290  evl1gsummul  22325  mat1scmat  22504  smadiadetlem4  22634  mptcoe1matfsupp  22767  chfacfscmulgsum  22825  chfacfpmmulgsum  22829  topbas  22937  neips  23078  lmbrf  23225  rnelfm  23918  tsmsres  24109  reconnlem1  24792  lmmbrf  25229  iscauf  25247  caucfil  25250  cmetcaulem  25255  voliunlem1  25517  isosctrlem1  26782  bcmono  27240  2lgslem1a  27354  dchrvmasumlem2  27461  mulog2sumlem2  27498  pntlemb  27560  nodense  27656  conway  27771  etaslts  27785  lesrec  27791  cofcutr  27916  precsexlem9  28207  usgr2pthlem  29831  2pthon3v  30011  elwspths2spth  30038  clwlkclwwlklem2fv2  30066  grpofo  30570  nvss  30664  nmosetn0  30836  hhsst  31337  pjoc1i  31502  chlejb1i  31547  cmbr4i  31672  pjjsi  31771  nmopun  32085  stlesi  32312  mdsl2bi  32394  mdslmd1lem1  32396  xraddge02  32830  supxrnemnf  32841  evlextv  33686  constrextdg2  33893  qtopt1  33979  lmxrge0  34096  esumcst  34207  sigagenval  34284  measdivcstALTV  34369  oms0  34441  ballotlemfc0  34637  ballotlemfcc  34638  bnj945  34916  bnj986  35097  bnj1421  35184  fv1stcnv  35959  fv2ndcnv  35960  fness  36531  nandsym1  36604  bj-finsumval0  37599  finixpnum  37926  poimirlem3  37944  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem27  37968  ismblfin  37982  ecxrn2  38729  lcvexchlem5  39484  paddssat  40260  dibn0  41599  lclkrs2  41986  aks4d1p1p7  42513  eqresfnbd  42673  fiphp3d  43247  pellqrex  43307  jm2.16nn0  43432  onexlimgt  43671  cantnf2  43753  rp-fakeanorass  43940  clsk1indlem2  44469  icccncfext  46315  wallispilem4  46496  fmtnorec1  48000  fmtnoprmfac1lem  48027  mod42tp1mod8  48065  stgoldbwt  48252  sbgoldbwt  48253  sbgoldbst  48254  evengpoap3  48275  wtgoldbnnsum4prm  48278  bgoldbnnsum3prm  48280  isubgruhgr  48344  uhgrimisgrgric  48407  isubgr3stgrlem7  48448  gpgprismgr4cycl0  48582  ply1mulgsumlem2  48863  ldepspr  48949  blennngt2o2  49068  inlinecirc02plem  49262