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

This theorem is referenced by:  jctr  524  ordunidif  6412  funtp  6604  dmtpos  8237  frrlem11  8295  oaabs2  8663  ixpsnf1o  8950  fodomr  9146  mapfienlem2  9423  cantnfrescl  9693  dfttrcl2  9741  cardprclem  9996  fin4en1  10326  ssfin4  10327  axdc3lem2  10468  axdc3lem4  10470  fpwwe2lem8  10655  recexsrlem  11120  nn0n0n1ge2b  12564  xmulpnf1  13279  ige2m2fzo  13721  swrdlsw  14643  swrd2lsw  14929  wrdl3s3  14939  lcmfass  16610  qredeu  16622  qnumdencoprm  16710  qeqnumdivden  16711  isacs1i  17630  subgga  19244  symgfixf1  19385  sylow1lem2  19547  sylow3lem1  19575  nn0gsumfz  19932  pzriprngALT  21414  evlsgsumadd  22030  evlsgsummul  22031  mhpmulcl  22066  mptcoe1fsupp  22127  evls1gsumadd  22236  evls1gsummul  22237  evl1gsummul  22272  mat1scmat  22434  smadiadetlem4  22564  mptcoe1matfsupp  22697  chfacfscmulgsum  22755  chfacfpmmulgsum  22759  topbas  22868  neips  23010  lmbrf  23157  rnelfm  23850  tsmsres  24041  reconnlem1  24735  lmmbrf  25183  iscauf  25201  caucfil  25204  cmetcaulem  25209  voliunlem1  25472  isosctrlem1  26743  bcmono  27203  2lgslem1a  27317  dchrvmasumlem2  27424  mulog2sumlem2  27461  pntlemb  27523  nodense  27618  conway  27725  etasslt  27739  slerec  27745  cofcutr  27837  precsexlem9  28106  usgr2pthlem  29570  2pthon3v  29747  elwspths2spth  29771  clwlkclwwlklem2fv2  29799  grpofo  30302  nvss  30396  nmosetn0  30568  hhsst  31069  pjoc1i  31234  chlejb1i  31279  cmbr4i  31404  pjjsi  31503  nmopun  31817  stlesi  32044  mdsl2bi  32126  mdslmd1lem1  32128  xraddge02  32520  supxrnemnf  32532  qtopt1  33430  lmxrge0  33547  esumcst  33676  sigagenval  33753  measdivcstALTV  33838  oms0  33911  ballotlemfc0  34106  ballotlemfcc  34107  bnj945  34398  bnj986  34580  bnj1421  34667  fv1stcnv  35366  fv2ndcnv  35367  fness  35827  nandsym1  35900  bj-finsumval0  36758  finixpnum  37072  poimirlem3  37090  poimirlem16  37103  poimirlem17  37104  poimirlem19  37106  poimirlem20  37107  poimirlem27  37114  ismblfin  37128  lcvexchlem5  38504  paddssat  39281  dibn0  40620  lclkrs2  41007  aks4d1p1p7  41539  eqresfnbd  41717  fiphp3d  42233  pellqrex  42293  jm2.16nn0  42419  onexlimgt  42665  cantnf2  42748  rp-fakeanorass  42937  clsk1indlem2  43466  icccncfext  45269  wallispilem4  45450  fmtnorec1  46871  fmtnoprmfac1lem  46898  mod42tp1mod8  46936  stgoldbwt  47110  sbgoldbwt  47111  sbgoldbst  47112  evengpoap3  47133  wtgoldbnnsum4prm  47136  bgoldbnnsum3prm  47138  ply1mulgsumlem2  47449  ldepspr  47535  blennngt2o2  47659  inlinecirc02plem  47853

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »