Theorem jca 310

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 153	. 2 |- (ph -> -. (ps -> -. ch))
4		df-an 242	. 2 |- ((ps /\ ch) <-> -. (ps -> -. ch))
5	3, 4	sylibr 217	1 |- (ph -> (ps /\ ch))

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

This theorem is referenced by:  jca31 311  jca32 312  jcai 313  jctl 314  jctr 315  jctil 316  jctir 317  ancli 320  ancri 321  anim12i 360  jaob 467  pm4.43 477  ancom 482  sylanbrc 527  syl2ancOLD 528  abai 537  ordi 656  ordiOLD 657  jcad 661  pm5.18OLD 723  pm4.82 811  prlem2 850  rnlem 853  dn1 855  dn1OLD 856  syl22anc 1101  syl112anc 1104  syl121anc 1105  syl211anc 1106  syl23anc 1107  syl122anc 1109  syl212anc 1110  syl221anc 1111  syl222anc 1116  syl123anc 1117  syl213anc 1118  syl231anc 1119  syl223anc 1123  syl232anc 1124  syl322anc 1125  syl233anc 1126  syl323anc 1127  syl332anc 1128  19.26 1416  19.40 1447  eu2 1791  mooran2 1824  mooran2OLD 1825  euan 1827  2eu1 1853  2eu3 1855  2eu6 1858  r19.26 2219  r19.40 2234  eqvinc 2387  reu6 2443  reu3 2444  ssinOLD 2815  unineq 2844  undif3 2854  un00 2907  prssOLD 3139  prel12 3155  preqsn 3157  uniintsn 3253  opthwiener 3554  itlso 3619  elon2 3668  unexb 3797  opeluu 3805  euuni 3807  rabsnt 3821  suceloni 3894  ordsucelsuc 3902  dflim3OLD 3931  opthprc 4046  xpsspw 4093  ideqg 4114  ideqgOLD 4115  resiexg 4253  elimasni 4292  asymref2OLD 4311  dminss 4330  imainss 4331  xpnz 4335  ssxpb 4346  relrelss 4417  dffun8OLD 4449  funopg 4454  fun11uni 4483  resfunexg 4500  funssxp 4577  ffdm 4578  f00 4601  dffo2 4621  fodmrnu 4626  foco 4628  dff1o2OLD 4640  f1ocnvOLD 4652  f1o00 4668  fv3 4690  dff2 4789  dff3 4790  dffo4 4793  ffnfv 4801  fsn2 4809  fconstfv 4825  f1ocnvfv1 4854  f1ocnvfv2 4855  isocnv 4873  isotr 4874  isotrALT 4875  eqop 5044  1stconst 5070  2ndconst 5071  curry1 5075  curry2 5078  oalim 5212  omlim 5213  oelim 5214  oalimcl 5242  oaass 5243  omordi 5245  omlimcl 5257  oen0 5261  oeordi 5262  oeordsuc 5269  mapval2 5394  map0 5403  bren2 5448  ac6sfilem2 5507  ac6sfilem3 5508  ac6sfi 5509  sdomex 5536  mapenlem2 5584  mapxpen 5589  xpmapenlem2 5591  xpmapenlem4 5593  xpmapenlem5 5594  mapunen 5596  onomeneq 5612  omsdomnn 5623  unblem1 5633  unfilem1 5641  unifi 5648  supsnALT 5682  ordiso 5683  ordtypelem6 5689  infensuc 5745  noinfep 5747  r1val1 5769  rankr1 5785  omsubindss 5888  aceq3 5895  ac6lem 5916  fodomb 5962  brdom3 5963  sucxpdom 5998  ondomon 6008  ltsopi 6168  addcmpblnq 6204  addclpq 6210  addasspq 6215  distrpqlem 6218  distrpq 6219  1qec 6220  ltsopq 6227  ltbtwnpq 6236  1pr 6269  prlem934 6291  reclem2pr 6309  reclem3pr 6310  supexpr 6315  mulclsr 6345  mulasssr 6351  distrsr 6352  ltsosr 6355  recexsrlem 6364  suppsrlem 6373  suprelem 6411  axmulass 6431  axdistr 6432  ltso 6681  xrltso 6729  xrrebnd 6743  mullt0 6870  mulnzcnopr 6891  divmuldiv 6956  divadddiv 6960  lemul1 7011  ltmul12a 7023  lemul12a 7026  lemulge11 7030  lediv1OLD 7034  lt2mul2div 7054  ltdiv2 7070  ltrec1 7071  lerec2 7072  ledivdiv 7073  lediv2 7074  ltdiv23 7075  lediv23 7076  lediv12a 7079  lediv2a 7080  recgt1i 7083  recreclt 7085  ledivp1 7088  nndivre 7135  nnleltp1 7138  nndivtr 7144  halfaddsubcl 7226  halfaddsub 7227  lt2halves 7228  rpregt0 7242  rprene0 7244  rpcnne0 7245  nnrecl 7281  xrsupsslem 7285  xrinfmsslem 7286  supxrunb1 7298  supxrunb2 7299  dfn2 7321  nn0ltp1le 7336  nn0addge1 7339  nn0addge2 7340  elnnz1 7364  elnn0nn 7380  elnnnn0b 7382  elnnnn0c 7383  zltp1le 7390  zdivadd 7398  zdivmul 7399  z2ge 7400  zextle 7401  peano2uz2 7413  uzind 7417  btwnz 7428  uzwo3lem1 7429  qre 7439  qaddcl 7449  qnegcl 7450  qmulcl 7451  qreccl 7453  irradd 7457  irrmul 7458  qbtwnre 7459  quoremz 7492  quoremnn0ALT 7493  quoremnn0 7494  intfracq 7496  fldiv 7497  fldiv2 7498  flmulnn0 7508  flmulnn0OLD 7509  modmulnn 7510  modid2 7513  elioo4g 7553  ioomax 7561  uzss 7600  eluzp1m1 7602  elfz5 7644  elfz2nn0 7667  fzss1 7675  fzss2 7676  fzrev2 7690  fzrev2i 7691  fsequb 7702  seq1rn 7735  seqzeq 7798  seqzrn 7800  expgt1 7834  exprecOLD 7838  exple1 7852  expubnd 7853  le2sq2 7877  bernneq 7898  bernneqOLD 7899  expnbnd 7901  expnlbnd 7902  digit2 7904  nn0opthi 7916  sqrlei 7957  sqrlti 7958  crui 7987  crre 8019  crim 8020  recj 8068  cj11OLD 8081  abs00i 8093  sqabs 8120  abslti 8127  abslei 8128  lenegsq 8137  cvganz 8176  facdiv 8194  facndiv 8195  faclbnd6 8206  fsum1ps 8278  fsumsplit 8280  fsumadd 8282  fsumshft 8291  fsumshftm 8292  fsumconst 8298  fsumabs2mul 8304  serzmulci 8318  binomlem5 8330  clm3i 8339  clm4lei 8341  climunii 8358  2climnn 8362  2climnn0 8363  climrecl 8370  climge0 8372  climaddlem3 8376  climaddc2 8379  climmullem1 8380  climmullem2 8381  climmullem3 8382  climmullem4 8383  climmullem5 8384  climmullem8 8387  climsub 8390  iserzmulc1 8396  climcmplem 8397  clim2serzi 8405  climserzlei 8407  climabslem 8408  climubii 8413  climcaui 8416  caucvg3ai 8424  caucvg3lem 8426  iserzabslem 8438  cvgcmp2lem 8440  cvgcmp2clem 8442  cvgcmp2clemOLD 8443  cvgcmpi 8445  cvgcmpubi 8446  isum1p 8467  isummulc1iALT 8474  reccnv 8479  infcvglem2 8483  infcvglem3 8484  arisumi 8487  geolimilem 8497  georeclim 8502  geoisum1c 8507  cvgratlem1 8512  cvgratlem5 8516  fsum0diaglem2 8519  elcncf1di 8532  mulc1cncf 8541  efcltlem1 8566  efseq0ex 8573  erelem2 8582  erelem3 8583  efcji 8598  efaddlem5 8604  efaddlem6 8605  efaddlem9 8608  efaddlem17 8616  efaddlem27 8626  ef1tllem 8643  ef01tllem1 8645  absef01tllem 8649  eirrlem2 8652  eirrlem4 8654  abspef01tlubi 8660  absefm1lei 8677  reeff1o 8691  sincl 8696  coscl 8697  efieq 8715  sin01bndlem2 8734  sin01bndlem3 8735  cos01bndlem2 8736  cos01bndlem3 8737  sincos1sgn 8745  demoivre 8752  acdc2lem1 8757  acdc2lem2 8758  acdc5lem1 8760  acdclem 8763  znnen 8771  infpnlem2 8776  infxpidmlem7 8827  infxpidmlem10 8830  infxpidmlem11 8831  infxpidmlem12 8832  infmap2lem2 8849  infmap2 8850  eltopsp 8873  tpsex 8874  istps 8875  tgcl 8894  tgss2 8907  basgen2 8909  fctop 8920  cctop 8922  elcls 8980  opnssneib 9005  neissex 9014  islp2 9023  clslp 9024  cnpco 9046  cnconst 9057  ismsg 9077  ismsi 9078  ismeti 9079  bl2in 9120  ssblex 9133  opni3 9143  blssopn 9144  lpbl 9157  metequiv 9158  lmbr 9206  lmnn 9213  iscauf 9217  lmuni 9229  lmsslem 9230  lmfexlem3 9236  lmle 9238  metelcls 9243  metcnp4 9248  lmcau 9274  cmsss 9275  bcthlem8 9284  bcthlem9 9285  bcthlem10 9286  bcthlem13 9289  bcthlem14 9290  bcthlem16 9292  bcthlem17 9293  bcthlem18 9294  bcthlem19 9295  bcthlem21 9297  isgrpi 9322  grpideu 9333  isgrp2i 9360  gxnn0neg 9386  gxadd 9398  gxnn0mul 9400  gxmodid 9402  ablmuldiv 9415  ablmul 9439  ghgrpilem3 9443  gafo 9451  isga2 9452  gaid 9454  ssga 9455  cnring 9489  vcex 9531  isvc 9532  isvci 9533  vacnlem3 9669  vacnlem5 9671  vacnlem6 9672  sspval 9721  sspz 9733  nmoub3i 9775  isblo3i 9801  blocnilem 9804  ubthlem4 9875  ubthlem9 9880  ubthlem10 9881  ubthlem11 9882  ubthlem12 9883  ubthlem12OLD 9884  ubthlem13 9885  ubthlem13OLD 9886  minveclem24 9913  minveclem26 9915  minveclem27 9916  minveclem28 9917  minveclem31 9920  htthlem6 9972  htthlem8 9974  psdmrn 9991  spwpr4 10006  sincosq1sgn 10053  sinq12gt0t 10057  efifolem7 10082  efif1lem3 10086  shftefif1olem 10095  eff1i 10098  oprabopabf 10157  unfin 10166  cdrci 10182  ghomid 10197  2txcn 10229  hmeobc 10239  subtopmetlem 10255  filintf 10274  oefil2 10275  fsubbas 10281  fbunfip 10282  fbssfg 10285  fgfil 10290  extbas1 10291  sfvlim 10296  neifil 10302  hausfillim 10303  elfilmap3 10314  isflimf 10323  tosdir 10358  exidu1 10373  ismnd1 10391  ring1cl 10415  isdivrng 10417  zrdivrng 10418  bcsiALT 10679  hlimuniii 10741  hhsssh 10772  ocsh 10789  ocin 10802  occllem6 10811  projlem2 10820  projlem25 10843  projlem26 10844  dfch2 10882  ococin 10930  shlubi 10979  shslubi 10991  shs00i 11006  chj00i 11043  spansnmul 11120  pjspansn 11133  spanunsni 11135  fh1 11194  fh2 11195  cm2j 11196  osumlem3 11215  5oalem5 11238  pjorthi 11249  pjssmii 11261  pjid 11275  pjjsi 11280  pjoi0 11297  eigposi 11399  eigvec1 11523  eighmre 11524  eighmorth 11525  lnophsi 11563  nmcopexlem5 11592  lncnopbd 11603  nmcfnexlem5 11621  riesz3i 11632  cnlnadjlem2 11638  cnlnadjeui 11647  nmopcoadji 11671  branmfn 11675  branmfnOLD 11676  rnbra 11678  leopmuli 11704  leopmul 11705  pjnmopi 11719  hmopidmchi 11723  pjhmopidm 11754  elpjch 11761  pjin2i 11766  hstoc 11794  hstnmoc 11795  hstle 11802  hstoh 11804  strlem3a 11824  strlem6 11828  hstrlem3a 11832  hstrlem6 11836  dmdbr5 11880  mdslj1i 11891  mdslj2i 11892  mdsl2bi 11895  mdslmd1lem1 11897  mdslmd1lem2 11898  mdexchi 11907  h1da 11921  cvbr3i 11939  atomli 11954  atcvatlem 11957  atcvat4i 11969  mdsymlem2 11976  mdsymlem5 11979  mdsymi 11983  sumdmdii 11987  cdj1i 12005  addltmulALT 12018  bnj236 12076  bnj168 12496  bnj214 12508  bnj563 12541  bnj566 12544  bnj1050 12889  bnj1074 12903  bnj1098 12917  bnj1195 12976  bnj1214 12988  bnj1304 13047  bnj109 13226  bnj129 13239  bnj545 13271  bnj546 13272  bnj547 13273  bnj548 13274  bnj557 13281  bnj569 13287  bnj578 13291  bnj605 13292  bnj583 13296  bnj607 13304  bnj849 13318  bnj966 13348  bnj967 13349  bnj1053 13396  bnj1067 13399  bnj1097 13412  bnj1099 13413  bnj1118 13420  bnj1173 13441  bnj1398 13515  bnj1312 13557  modaddabs 13612  lediv2aALT 13621  ghomf1olem 13637  dvdscmul 13680  dvdsmulc 13681  dvdscmulr 13682  dvdsmulcr 13683  dvds2ln 13684  divalg2 13708  ndvdssub 13710  ndvdsadd 13711  gcdcllem1 13718  gcd0id 13729  algfx 13748  mulgcdlem2 13757  mulgcdlem3 13758  mulgcdlem4 13759  zgt1b1 13771  zgt1b3 13773  dfon2 13858  poxp 13949  wfrlem4 13960  wfrlem5 13961  wfrlem15 13971  sltval2 13997  axfelem13 14043  axfelem14 14044  axfelem15 14045  axfelem16 14046  altxpsspw 14100  df3nandALT1 14146  waj-ax 14238  nndivsub 14258  nndivlub 14259  nxtand 14313  oprabex2gpop 14337  surrc2 14390  restidsing 14391  twsymr 14394  sndw 14428  eqfnung2 14459  surjsec 14462  inpreima2 14468  fopab2g 14485  mapmapmap 14486  injsurinj 14487  repcpwti 14503  cbicplem 14508  prjmapcp2 14515  dstr 14516  iscst1 14519  jidd 14540  midd 14541  domrancur1b 14548  domrancur1c 14550  valcurfn1 14552  prltub 14602  ubpar 14603  supaub 14615  geme2 14617  inposet 14620  definc 14621  domncnt 14624  ranncnt 14625  dutos1 14626  tolat 14631  pospos 14635  tostos 14637  toplat 14638  dfdir2 14639  latdir 14643  mgmlion 14697  clfsebs 14707  fprodadd 14713  expus 14726  ltlga 14729  symgfo 14730  gaplc 14731  curgrpact 14735  grpdivfo 14737  grpdlcan 14739  trinv 14759  zerdivemp1 14785  mvecrtol2 14820  mulinvsca 14823  svli2 14826  svs2 14829  truni1 14849  truni3 14851  cbci 14852  topindis 14859  clsint 14860  inttop2 14863  mapdiscnlem 14870  mapudiscn 14872  osneisi 14875  hmpher 14890  hmeogrp 14892  homcard 14893  homindlem3 14900  qusp 14908  fgsb 14921  fgsb2 14925  efilcp2 14926  cnfilca 14927  rcfpfillem3 14930  rcfpfil 14934  limfilnei 14943  iscnp3 14946  t2t1 14949  stfincomp 14959  bwt2 14960  singempcon 14965  istopgrp 14971  idtrgrp 14978  invtrgrp 14979  cnvtrhom 14984  trhom2 14985  altretop 14997  cntrsetlem 14999  mslb1 15007  2wsms 15008  msra3 15009  iintlem1 15010  iint 15012  trnij 15015  cnvtr 15016  lvsovso 15038  lvsovso2 15039  aidm2 15097  dmrngcmp 15098  cmpmorp 15126  dualcat2 15133  eqidob 15144  cmpassoh 15150  imonclem 15162  cmpmon 15164  idmon 15166  immon 15167  iepiclem 15172  idfisf 15189  issubcat 15193  idsubfun 15206  taralt 15211  tarax3d2 15225  tarsuc1 15244  intartar 15255  tartarmap 15265  eltintpar 15276  inttaror 15277  fnctartar 15284  fnctartar2 15285  isline1 15294  finminlem 15367  finsschain 15373  ordisoOLD 15374  ordtypelem6OLD 15380  omsubindssOLD 15397  opncldf2 15403  opncldf3 15404  ntrin 15411  clsun 15413  neiin 15418  subcls 15424  cnsubsp 15426  compsub 15431  cptclsscpt 15432  uncomp 15433  alexsublem3 15439  alexsublem4 15440  alexsub 15441  dfcon2 15442  reconnlem1 15446  reconnlem2 15447  reconnlem3 15448  reconnlem4 15449  reconnlem5 15450  ivthALT 15454  2ndcctbss 15478  isfne 15480  isref 15488  topfneec 15501  islocfin 15506  locfincomp 15514  locfindsc 15515  comppfsc 15517  neibastop1 15518  neibastop2lem3 15521  neibastop3 15524  topmeet 15526  topjoin 15527  fnemeet1 15528  fnemeet2 15529  isnrm2 15552  opnfbas 15557  supfil 15560  isufil2 15565  filssufil 15571  fixufil 15576  ufinffr 15578  ufilen 15579  filcon 15580  ufcondr 15581  limfilcf 15587  cnpfillim 15589  fmfnfmlem4 15597  isfclus 15606  flimfcls 15613  fcluscnp 15618  fcluscomplem 15620  filnetlem4 15643  filnet 15645  anim12da 15647  cocanfo 15689  difxp 15690  eqfnun 15705  upixp 15729  welb 15759  pofun 15772  fzmul 15790  fzdisj 15793  elnnr 15803  sdclem1 15809  sdc 15811  fsumltisumi 15823  fsumleisumii 15825  csbrni 15832  trirni 15833  metf1o 15843  blssp 15844  mettrifi 15847  geomcau 15849  lincmb01icc 15879  txmet 15925  bndss 15942  ismtycnv 15949  ismtyhmeolem 15950  ismtyhmeo 15951  heiborlem1 15955  heiborlem10 15964  heiborlem30 15984  heiborlem32 15986  heiborlem36 15990  heibor 15997  bfplem6 16003  bfplem8 16005  rrnmet 16016  rrndstprj1 16017  rrndstprj2 16018  rrncms 16019  rrntotbndlem2 16021  rrntotbnd 16022  exidreslem 16030  isgrpda 16033  ghomco 16040  ghomdiv 16041  phtpyid 16049  phtpycom 16050  phtpyco 16056  phtpcer 16062  reparpht 16065  pcohtpy 16083  pcoass 16085  pcorev 16087  pi1gp 16095  isringd 16097  ringnegmn1l 16102  ringnegmn1r 16103  ringsubdi 16106  ringsubdir 16107  zerdivemp1x 16108  isdivrng2 16111  rnghomco 16128  rngisocnv 16135  iscringd 16147  isfld2 16153  idlsubcl 16171  rngidl 16172  0idl 16173  intidl 16177  inidl 16178  unichnidl 16179  keridl 16180  prnc 16215  prter1 16282  prter2 16285  pm10.55 16316  pm11.57 16346  pm11.58 16347  addrcom 16475  strdif 16719  lubid 16807  islati 16854  latjcom 16860  latmcom 16870  latjass 16886  isclati 16892  atomcmp 17008  hlexch3 17041  hlexch4 17042  cvr1 17054  atcvrj2b 17069  atexchcvr 17073  cvrat4 17076  ps-1 17078  ps2 17079  grpideuNEW 17114  isgrpiNEW 17115  pointpsub 17231  pmapglb2 17253  pmapglb2x 17254  paddasslem2 17282  paddasslem4 17284  paddasslem7 17287  paddasslem9 17289  paddasslem10 17290  paddasslem15 17295  pmodi 17309  pmod 17311  paddun 17337  poml5 17362  osumcllem11 17374  osumcl 17375  pexmidlem6 17383  pexmidlem8 17385  pl42lem1 17407  pl42lem2 17408

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 164  df-an 242

Copyright terms: Public domain