Theorem jca 286

Description: Deduce conjunction of the consequents of two implications ("join consequents with 'and'").

Hypotheses

Ref	Expression
jca.1	|- (ph -> ps)
jca.2	|- (ph -> ch)

Assertion

Ref	Expression
jca	|- (ph -> (ps /\ ch))

Proof of Theorem jca

Step	Hyp	Ref	Expression
1		jca.1	. . 3 |- (ph -> ps)
2		jca.2	. . 3 |- (ph -> ch)
3	1, 2	jc 136	. 2 |- (ph -> -. (ps -> -. ch))
4		df-an 223	. 2 |- ((ps /\ ch) <-> -. (ps -> -. ch))
5	3, 4	sylibr 198	1 |- (ph -> (ps /\ ch))

Syntax hints:  -. wn 2   -> wi 3   /\ wa 221

This theorem is referenced by:  jcai 287  jctl 288  jctr 289  jctil 290  jctir 291  ancli 294  ancri 295  anim12i 331  jaob 422  pm4.43 432  ancom 437  syl2anc 475  abai 482  impbid 519  ordi 599  jcad 603  pm5.18 663  pm4.82 744  ecase2d 756  dn1 779  3jca 825  ecase23d 929  19.26 1103  19.40 1130  a4imed 1198  sb2 1214  sbequ1 1215  sbn 1268  eu2 1435  mooran2 1465  2eu1 1489  2eu3 1491  2eu6 1494  r19.40 1808  reu3 1977  reu6 1978  eqssd 2131  ssrabdv 2178  psstr 2202  ssin 2284  unineq 2307  un00 2359  raaan 2414  prss 2536  prel12 2549  preqsn 2551  opthwiener 2884  itlso 2942  wereu 2972  elon2 2986  ordelord 2997  ordnbtwn 3062  unexb 3096  opeluu 3103  euuni 3105  reucl2 3111  rabsnt 3117  suceloni 3170  dflim3 3201  ordom 3228  omssnlim 3232  opthprc 3306  xpsspw 3346  ideqg 3366  resiexg 3486  asymref2 3532  dminss 3547  imainss 3548  xpnz 3551  ssxpb 3560  relssdmrn 3617  relrelss 3618  dffun8 3645  funopg 3652  funun 3659  fununi 3668  fun11uni 3670  resfunexg 3685  fnco 3701  fnopabg 3722  fss 3742  fco 3743  funssxp 3745  ffdm 3746  f00 3764  dffo2 3783  fodmrnu 3788  foco 3790  dff1o2 3801  f1f1orn 3807  f1ocnv 3809  foimacnv 3814  f1o00 3825  fv3 3844  dff2 3930  dff3 3931  dffo4 3934  fopab2 3937  ffnfv 3942  fsn2 3950  fconstfv 3963  f1ocnvfv1 3992  f1ocnvfv2 3993  isocnv 4010  isotr 4011  isotrALT 4012  f1oiso 4018  fnoprabg 4072  1stcof 4160  eqop 4164  1stconst 4190  2ndconst 4191  curry1 4193  curry2 4196  tfrlem12 4223  oalim 4303  omlim 4304  oelim 4305  oalimcl 4330  oaass 4331  omordi 4333  omlimcl 4345  oen0 4349  oeordi 4350  oewordri 4355  oeordsuc 4357  omsmo 4397  mapval2 4476  map0 4485  bren2 4530  en2d 4541  dom2d 4545  ac6sfilem2 4589  ac6sfilem3 4590  ac6sfi 4591  sbthlem9 4600  sdomex 4618  fodomr 4628  mapenlem2 4637  mapxpen 4642  xpmapenlem2 4644  xpmapenlem4 4646  xpmapenlem5 4647  mapunen 4649  php2 4661  php3 4662  onomeneq 4665  omsdomnn 4676  unblem1 4686  unblem4 4689  unfilem1 4694  unifi 4701  supmo 4719  supmax 4732  suppr 4733  supsnALT 4735  infensuc 4784  noinfep 4786  r1ord 4801  r1val1 4804  rankr1 4820  aceq3 4879  ac6lem 4900  fodom 4944  fodomb 4946  brdom3 4947  sucxpdom 4996  cardsdomel 5002  ondomon 5006  ondomcard 5007  carduni 5008  cardmin 5010  ltsopi 5170  addclpi 5174  mulclpi 5175  addcmpblnq 5206  addclpq 5212  addasspq 5217  distrpqlem 5220  distrpq 5221  1qec 5222  ltsopq 5229  ltexpq 5234  ltbtwnpq 5238  genpcl 5265  1pr 5271  prlem934 5293  ltexprlem5 5300  reclem2pr 5311  reclem3pr 5312  supexpr 5317  mulclsr 5347  mulasssr 5353  distrsr 5354  ltsosr 5357  recexsrlem 5366  suppsrlem 5375  suprelem 5413  axmulass 5432  axdistr 5433  ltxrlt 5654  ltso 5666  xrltso 5708  xrrebnd 5722  xrre 5723  mullt0 5835  mulnzcnopr 5854  divmuldiv 5919  divadddiv 5923  divdivdiv 5924  conjmul 5937  lemul1 5973  ltmul12a 5985  lemul12a 5988  lemulge11 5992  lediv1OLD 5996  lt2mul2div 6016  ltdiv2 6032  ltrec1 6033  lerec2 6034  ledivdiv 6035  lediv2 6036  ltdiv23 6037  lediv23 6038  lediv12a 6041  lediv2a 6042  recgt1i 6045  recp1lt1 6046  recreclt 6047  ledivp1 6050  nndivre 6097  nnleltp1 6100  nndivtr 6106  halfaddsubcl 6186  halfaddsub 6187  lt2halves 6188  nnrp 6197  rpregt0 6201  rprene0 6203  rpcnne0 6204  rpaddcl 6206  rpmulcl 6207  rpdivcl 6208  lbinfm 6216  nnrecl 6240  xrsupsslem 6244  xrinfmsslem 6245  supxrunb1 6257  supxrunb2 6258  dfn2 6280  nn0ltp1le 6295  nn0addge1 6298  nn0addge2 6299  nnnegz 6306  elnnz 6313  elnnz1 6323  elnn0nn 6339  elnnnn0b 6341  elnnnn0c 6342  zltp1le 6349  zdivadd 6357  zdivmul 6358  z2ge 6359  zextle 6360  gtndiv 6364  msqznn 6367  peano2uz2 6372  uzind 6376  uzindOLD 6379  uzwo5OLD 6382  btwnz 6387  uzwo3lem1 6388  qre 6398  qaddcl 6408  qnegcl 6409  qmulcl 6410  qreccl 6412  irradd 6416  irrmul 6417  qbtwnre 6418  flid 6433  flval2 6437  flval3 6438  flge0nn0 6441  flge1nn 6442  fladdz 6443  quoremz 6451  quoremnn0ALT 6452  quoremnn0 6453  intfracq 6455  fldiv 6456  fldiv2 6457  flmulnn0 6467  flmulnn0OLD 6468  modmulnn 6469  zmodcl 6470  modid 6471  modid2 6472  modabs 6473  elioo4g 6511  eliooord 6514  ioomax 6519  uzss 6558  eluzp1m1 6560  eluzaddi 6563  eluzsubi 6564  uzind4 6577  elfz5 6602  eluzfz1 6615  eluzfz2 6617  elfznn 6624  elfz2nn0 6625  elfznn0 6626  fzss1 6633  fzss2 6634  elfzp1 6641  fzrev2 6643  fzrev2i 6644  fzrev3 6645  fsequb 6654  seq1rn 6687  shftf 6716  seqzeq 6750  seqzrn 6752  expgt1 6786  exprec 6789  exprecOLD 6790  expsub 6793  expordi 6797  expword2i 6802  expmwordi 6803  exple1 6804  expubnd 6805  le2sq2 6829  bernneq 6849  bernneqOLD 6850  expnbnd 6852  expnlbnd 6853  digit2 6855  nn0opthi 6867  sqrlei 6908  sqrlti 6909  rpsqrcl 6916  sqr2irrlem1 6925  crui 6938  replim 6962  crre 6970  crim 6971  recj 7019  cj11OLD 7032  abs00i 7044  absrpcl 7057  sqabs 7071  abslti 7078  abslei 7079  nn0abscl 7082  lenegsq 7088  abs2dif 7105  abs2difabs 7106  abs1mi 7107  cvganz 7127  facdiv 7145  facndiv 7146  faclbnd 7148  faclbnd6 7157  bcnp11 7168  permnn 7176  fsum1ps 7221  fsumsplit 7223  fsumadd 7225  fsumshft 7234  fsumshftm 7235  fsumconst 7241  fsumabs2mul 7247  serzmulci 7261  binomlem5 7273  clm3i 7282  clm4lei 7284  climunii 7301  2climnn 7305  2climnn0 7306  climrecl 7313  climge0 7315  climaddlem3 7319  climaddc1 7321  climaddc2 7322  climmullem1 7323  climmullem2 7324  climmullem3 7325  climmullem4 7326  climmullem5 7327  climmullem8 7330  climsub 7333  climsubc2 7334  clim2serz 7337  iserzmulc1 7339  climcmplem 7340  clim2serzi 7348  climserzlei 7350  climabslem 7351  climubii 7356  climcaui 7359  caucvg3ai 7367  caucvg3lem 7369  iserzabslem 7381  cvgcmp2lem 7383  cvgcmp2clem 7385  cvgcmp2clemOLD 7386  cvgcmpi 7388  cvgcmpubi 7389  isum1p 7410  iserzgt0 7415  isummulc1iALT 7417  reccnv 7422  infcvglem2 7426  infcvglem3 7427  arisumi 7430  geolimilem 7440  georeclim 7445  geoisum1c 7450  cvgratlem1 7455  cvgratlem2 7456  cvgratlem5 7459  fsum0diaglem2 7462  fsum0diag4 7466  elcncf1di 7475  mulc1cncf 7484  ivthlem7 7492  efcltlem1 7509  efseq0ex 7516  erelem2 7525  erelem3 7526  efcji 7541  efaddlem2 7544  efaddlem5 7547  efaddlem6 7548  efaddlem9 7551  efaddlem10 7552  efaddlem17 7559  efaddlem27 7569  efsub 7576  ef1tllem 7586  ef01tllem1 7588  absef01tllem 7592  eirrlem2 7595  eirrlem4 7597  abspef01tlubi 7603  reeff1 7618  absefm1lei 7620  efcn 7631  reeff1o 7634  sincl 7639  coscl 7640  efi4p 7643  efieq 7658  sin01bndlem2 7677  sin01bndlem3 7678  cos01bndlem2 7679  cos01bndlem3 7680  sincos1sgn 7688  demoivre 7695  acdc2lem1 7700  acdc2lem2 7701  acdc5lem1 7703  acdclem 7706  znnen 7714  infpnlem2 7719  infxpidmlem7 7770  infxpidmlem10 7773  infxpidmlem11 7774  infxpidmlem12 7775  infmap2lem2 7792  infmap2 7793  eltopsp 7816  tpsex 7817  istps 7818  istps2 7819  tgcl 7836  tgss2 7849  basgen2 7851  subtop 7858  indistop 7860  cctop 7862  elcls 7914  neiss 7933  opnneissb 7938  opnssneib 7939  ssnei2 7940  innei 7946  neissex 7948  islp2 7957  clslp 7958  idcn 7976  cnco 7978  cnpco 7979  cnconst 7990  dnsconst 7998  ismsg 8010  ismsi 8011  ismeti 8012  metsym 8026  bl2in 8053  blcntr 8055  blss 8063  ssblex 8066  opnm 8070  opni3 8076  blssopn 8077  opntop 8080  blnei 8089  lpbl 8090  metequiv 8091  methausi 8092  metcnp 8098  tgioolem 8125  tgioo 8126  lmbr 8139  lmnn 8146  iscauf 8150  lmuni 8162  lmsslem 8163  lmfexlem3 8169  lmle 8171  metelcls 8176  metcnp4 8181  xplm 8186  xpcn 8187  lmcau 8207  cmsss 8208  bcthlem8 8217  bcthlem9 8218  bcthlem10 8219  bcthlem13 8222  bcthlem14 8223  bcthlem16 8225  bcthlem17 8226  bcthlem18 8227  bcthlem19 8228  bcthlem21 8230  bcthlem26 8235  bcthlem30 8239  isgrpi 8255  grpidinv 8265  grpideu 8266  grprlidrid 8270  isgrp2i 8293  gxnn0neg 8319  gxadd 8331  gxnn0mul 8333  gxmodid 8335  ablmuldiv 8348  gxdi 8355  issubg 8358  ablmul 8372  ghgrpilem3 8376  cnring 8404  vcex 8446  isvc 8447  isvci 8448  nvex 8477  isnv 8478  nvpi 8541  nvabs 8548  nv1 8551  vacnlem3 8584  vacnlem5 8586  vacnlem6 8587  nmcnilem 8591  va1cnlem 8599  sm1cnilem 8601  sspval 8636  sspz 8648  nmoub3i 8690  nmblore 8701  0lno 8705  0blo 8707  nmlno0lem 8708  nmblolbii 8714  isblo3i 8716  blocnilem 8719  blocni 8720  ipasslem4 8749  sspph 8771  ipblnfi 8772  ubthlem3 8789  ubthlem4 8790  ubthlem9 8795  ubthlem10 8796  ubthlem11 8797  ubthlem12 8798  ubthlem12OLD 8799  ubthlem13 8800  ubthlem13OLD 8801  minveclem24 8828  minveclem25 8829  minveclem26 8830  minveclem27 8831  minveclem28 8832  minveclem30 8834  minveclem31 8835  minveclem32 8836  ssphl 8881  htthlem6 8887  htthlem8 8889  htthlem11 8892  psdmrn 8910  spwpr4 8925  spwpr4c 8928  sincosq1sgn 8971  sinq12gt0t 8975  sineq0 8983  sineq0OLD 8984  efifolem7 9000  efif1lem3 9004  shftefif1olem 9013  eff1i 9016  bcsiALT 9322  hlimuniii 9384  hhsssh 9415  ocsh 9432  ocin 9445  occllem6 9454  occli 9457  projlem2 9463  projlem10 9471  projlem25 9486  projlem26 9487  projlem29 9490  pjthlem10 9504  pjtheui 9511  dfch2 9525  ococin 9573  shlubi 9622  shslubi 9634  shs00i 9649  chj00i 9686  spansnmul 9763  pjspansn 9776  spanunsni 9778  fh1 9837  fh2 9838  cm2j 9839  osumlem3 9858  5oalem1 9877  5oalem2 9878  5oalem4 9880  5oalem5 9881  3oalem2 9886  pjorthi 9892  pjssmii 9904  pjid 9918  pjjsi 9923  pjoi0 9940  eigposi 10042  nmopre 10077  unopf1o 10120  cnvunop 10122  unoplin 10124  counop 10125  hmopadj2 10145  hmoplin 10146  bralnfn 10152  eigvec1 10166  eighmre 10167  nmlnop0iALT 10199  lnopmi 10204  lnophsi 10205  nmopun 10218  unopbd 10219  hmops 10224  hmopm 10225  hmopco 10227  nmcopexlem5 10234  nmophmi 10240  bdophmi 10241  lnopconi 10242  lncnopbd 10245  nmcfnexlem5 10263  lnfnconi 10269  riesz3i 10274  cnlnadjlem2 10280  cnlnadjlem7 10285  cnlnadjeui 10289  adjlnop 10298  nmopcoadji 10313  branmfn 10317  branmfnOLD 10318  rnbra 10320  leoprf2 10340  leopmuli 10346  leopmul 10347  leopnmid 10351  nmopleid 10352  pjnmopi 10355  hmopidmchi 10359  hmopidmpji 10360  pjhmopidm 10390  elpjch 10397  pjin2i 10402  pjclem4 10408  pj3si 10416  hstoc 10430  hstnmoc 10431  hstle 10438  hstoh 10440  stlesi 10449  strlem3a 10460  strlem6 10464  hstrlem3a 10468  hstrlem6 10472  dmdbr5 10516  mdslj1i 10527  mdslj2i 10528  mdsl2bi 10531  mdslmd1lem1 10533  mdslmd1lem2 10534  csmdsymi 10542  mdexchi 10543  h1da 10557  atom1d 10561  shatomistici 10569  cvbr3i 10575  atomli 10591  atcvatlem 10594  irredlem2 10600  atcvat3i 10605  atcvat4i 10606  mdsymlem2 10613  mdsymlem5 10616  mdsymi 10620  sumdmdii 10624  cdj1i 10642  cdj3i 10650  lediv2aALT 10656  ghomid 10679  ghomf1olem 10681  nndivsub 10706  nndivlub 10707  unfin 10797  njtlc 10804  restidsing 10805  twsymr 10808  jidd 10840  midd 10841  inposet 10868  definc 10869  domncnt 10872  ranncnt 10873  pospos 10882  tostos 10883  toplat 10884  opidon 10898  exidu1 10902  mndmgmid 10924  ismnd1 10927  ismnd2 10928  expus 10938  ring1cl 10966  isdivrng 10968  zrdivrng 10969  cdrci 10994  truni1 10999  truni3 11001  clint3 11002  cbci 11003  topindis 11009  clsint 11010  mapdiscn 11014  mapudiscn 11015  osneisi 11018  hmpher 11042  hmeogrp 11044  homcard 11045  hmeobc 11048  homindlem3 11053  qusp 11068  oefil2 11079  neifil 11080  filintf 11081  fgsb 11082  fgsb2 11086  efilcp2 11087  cnfilca 11088  rcfpfillem3 11091  rcfpfil 11095  sfvlim 11100  t2t1 11108  fintopcomp 11115  stfincomp 11122  bwt2 11123  singempcon 11134  altretop 11144  mslb1 11152  2wsms 11153  msra3 11154  iintlem1 11155  iint 11157  trnij 11160  cnvtr 11161  aidm2 11204  dmrngcmp 11205  cmpmorp 11233  eqidob 11250  cmpassoh 11256  imonclem 11268  cmpmon 11270  idmon 11272  immon 11273  iepiclem 11278  idfisf 11295  issubcat 11299  idsubfun 11312  jca31 11340  jca32 11341  eqeu 11394  finminlem 11418  fictb 11423  finsschain 11425  ordiso 11426  ordtypelem6 11432  ordtypelem7 11433  hartoglem 11435  hartog 11436  onsdom 11437  elomsubsd 11446  omsubindss 11449  infenomsub 11450  opncldf1 11454  opncldf2 11455  opncldf3 11456  ntrin 11463  clsun 11465  neiin 11470  cnpnei 11472  subcls 11481  cnsubsp 11483  compsublem 11487  compsub 11488  cptclsscpt 11489  uncomp 11490  hscptsscld 11491  compfipin0lem 11492  compfipin0 11493  cncomp 11494  alexsublem3 11498  alexsublem4 11499  alexsub 11500  dfcon2 11501  cnconn 11503  subtopmetlem 11505  subtopmet 11506  reconnlem1 11507  reconnlem2 11508  reconnlem3 11509  reconnlem4 11510  reconnlem5 11511  ivthALT 11515  2ndcctbss 11539  isfne 11541  isref 11549  fness 11552  ssref 11553  fnetr 11556  reftr 11558  topfneec 11562  topfneec2 11563  fnessref 11564  refssfne 11565  islocfin 11567  lfinpfin 11574  locfincomp 11575  locfindsc 11576  locfincf 11577  comppfsc 11578  neibastop1 11579  neibastop2lem3 11582  neibastop2lem4 11583  neibastop2 11584  neibastop3 11585  topmtcl 11586  topmeet 11587  topjoin 11588  fnemeet1 11589  fnemeet2 11590  fnejoin1 11591  fnejoin2 11592  ist1-2 11603  isnrm2 11613  opnfbas 11629  fsubbas 11630  fbunfip 11631  fbssfg 11635  fgfil 11638  extbas1 11641  neifg 11644  supfil 11645  isufil2 11650  filssufillem 11655  filssufil 11656  ufileulem 11657  ufileu 11658  filufint 11659  uffixfr 11660  fixufil 11661  ufinffr 11663  ufilen 11664  filcon 11665  ufcondr 11666  limfilcf 11683  flimcls 11684  hausfillim 11685  cnpfillim 11686  elfilmap3 11692  fmfnfmlem1 11700  fmfnfmlem4 11703  fmfnfm 11704  fmufil 11705  isflimf 11709  isfclus 11718  fcluscf 11724  flimfcls 11725  fclsfnflim 11726  flimfnfcls 11727  fcluscnp 11730  fcluscomplem 11732  tosdir 11755  filnetlem3 11765  filnetlem4 11766  filnetlem5 11767  filnet 11768  gafo 11773  isga2 11774  gaid 11776  ssga 11777  gapm 11784  sylanbrc 11786  difxp 11798  oprabopabf 11807  fnopabco 11810  oprabco 11811  upxp 11822  upixp 11823  welb 11851  rddif 11869  elnnr 11874  sdclem1 11875  sdc 11877  fsumltisumi 11886  fsumleisumii 11888  csbrni 11895  trirni 11896  metf1o 11907  blssp 11908  metsstop 11909  mettrifi 11912  geomcau 11914  metdcn 11918  lincmb01icc 11943  cnimass 11949  cnres 11950  cnresima 11952  paste 11954  tx1cn 11976  tx2cn 11977  uptx 11978  txcnopab 11980  2txcn 11982  bndss 11998  ismtycnv 12005  ismtyhmeolem 12006  ismtyhmeo 12007  heiborlem1 12011  heiborlem10 12020  heiborlem30 12040  heiborlem32 12042  heiborlem33 12043  heiborlem36 12046  heibor 12053  bfplem6 12059  bfplem8 12061  bfplem9 12062  recms 12066  rrnmet 12072  rrndstprj 12073  rrndstprj2 12074  rrncms 12075  rrntotbndlem2 12077  rrntotbnd 12078  iccbnd 12082  icccmp 12083  phtpyid 12091  phtpycom 12092  phtpyco 12098  phtpcdm 12103  phtpcer 12104  elequ3 12224

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 145  df-an 223

Copyright terms: Public domain