Theorem jca 288

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

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

This theorem is referenced by:  jcai 289  jctl 290  jctr 291  jctil 292  jctir 293  ancli 296  ancri 297  anim12i 333  jaob 422  pm4.43 431  ancom 435  syl2anc 472  abai 478  impbid 514  ordi 594  jcad 598  pm5.18 658  pm4.82 737  ecase2d 749  3jca 817  ecase23d 919  19.26 1063  19.40 1090  a4imed 1157  sb2 1173  sbequ1 1174  sbn 1226  eu2 1389  mooran2 1419  2eu1 1442  2eu3 1444  2eu6 1447  r19.40 1754  reu3 1921  reu6 1922  eqssd 2069  ssrabdv 2116  psstr 2140  ssin 2222  unineq 2245  un00 2296  raaan 2350  prss 2462  prel12 2475  preqsn 2477  opthwiener 2796  itlso 2854  unexb 2864  opeluu 2869  euuni 2871  reucl2 2878  rabsnt 2884  wereu 2935  elon2 2949  ordelord 2960  suceloni 3052  ordnbtwn 3053  dflim3 3108  ordom 3131  omssnlim 3135  opthprc 3211  xpsspw 3247  ideqg 3266  resiexg 3380  asymref2 3424  asymref2OLD 3426  dminss 3448  imainss 3449  xpnz 3452  ssxprOLD 3461  ssxpr 3462  relssdr 3499  dffun7 3526  funopg 3533  funun 3540  fununi 3549  fun11uni 3551  resfunexg 3565  fnco 3581  fnopabg 3601  fss 3620  fco 3621  funssxp 3623  ffdm 3624  f00 3642  dffo2 3660  fodmrnu 3665  foco 3667  f1o2 3678  f1f1orn 3684  f1ocnv 3686  f1o00 3699  fv3 3718  dff4 3801  dff2 3802  dffo4 3805  fopab2 3808  ffnfv 3813  fsn2 3821  fconstfv 3834  f1ocnvfv1 3863  f1ocnvfv2 3864  isocnv 3881  isotr 3882  isotrALT 3883  f1oiso 3889  tfrlem12 3907  fnoprabg 3997  2ndconst 4081  curry1 4082  1stcof 4085  eqop 4088  oalim 4151  omlim 4152  oelim 4153  oalimcl 4178  oaass 4179  omordi 4181  omlimcl 4193  oen0 4197  oeordi 4198  oewordri 4203  oeordsuc 4205  omsmo 4241  mapval2 4319  map0 4328  bren2 4370  en2d 4381  dom2d 4385  sbthlem9 4435  sdomex 4453  fodomr 4463  mapenlem2 4470  mapxpen 4475  xpmapenlem2 4477  xpmapenlem4 4479  xpmapenlem5 4480  mapunen 4482  php2 4494  php3 4495  onomeneq 4498  omsdomnn 4509  unblem1 4517  unblem4 4520  unfilem1 4524  unifi 4532  supmo 4550  suppr 4562  supsnALT 4564  infensuc 4610  noinfep 4612  r1ord 4627  r1val1 4630  rankr1 4646  aceq3 4705  ac6lem 4726  fodom 4770  fodomb 4772  brdom3 4773  sucxpdom 4818  cardsdomel 4824  ondomon 4828  ondomcard 4829  carduni 4830  cardmin 4832  ltsopi 4988  addclpi 4992  mulclpi 4993  addcmpblnq 5024  addclpq 5030  addasspq 5035  distrpqlem 5038  distrpq 5039  1qec 5040  ltsopq 5047  ltexpq 5052  ltbtwnpq 5056  genpcl 5083  1pr 5089  prlem934 5111  ltexprlem5 5118  reclem2pr 5129  reclem3pr 5130  supexpr 5135  mulclsr 5165  mulasssr 5171  distrsr 5172  ltsosr 5175  recexsrlem 5184  suppsrlem 5193  suprelem 5231  axmulass 5250  axdistr 5251  ltxrltt 5472  ltso 5484  xrltso 5527  xrrebndt 5541  xrret 5542  mulnzcnopr 5671  divmuldivt 5736  divcan5t 5737  divadddivt 5740  conjmult 5753  ltmul12it 5797  lemul12it 5800  lemulge11t 5804  lediv1t 5806  ltdiv2t 5835  ltrec1t 5836  lerec2t 5837  ledivdivt 5838  lediv2t 5839  lediv12it 5844  lediv2it 5845  recgt1it 5848  recp1lt1 5849  recrecltt 5850  ledivp1t 5853  nnleltp1t 5901  nndivtrt 5907  halfaddsubcl 5987  halfaddsubt 5988  lt2halvest 5989  lbinfm 5995  nnreclt 6019  xrsupsslem 6023  xrinfmsslem 6024  supxrunb1 6036  supxrunb2 6037  dfn2 6059  nn0ltp1let 6074  nn0addge1t 6077  nn0addge2t 6078  nnnegz 6085  elnnz 6092  elnnz1 6102  elnn0nn 6118  elnnnn0b 6120  elnnnn0c 6121  zltp1let 6128  z2get 6135  zextlet 6136  gtndivt 6140  msqznn 6143  peano2uz2 6149  uzind 6153  uzindOLD 6156  uzwo5OLD 6159  btwnz 6163  uzwo3lem1 6164  flidt 6180  flval2t 6181  flval3t 6182  flge0nn0t 6185  flge1nnt 6186  fladdzt 6187  qret 6197  qnegclt 6208  qrecclt 6211  qbtwnre 6216  rpaddclt 6227  rpmulclt 6228  rpdivclt 6229  seq1rn 6259  shftf 6288  elioo4g 6318  ioomax 6325  ioossicc 6330  uzss 6363  eluzp1m1t 6365  eluzaddi 6368  eluzsubi 6369  uzind4 6382  elfz5t 6406  eluzfz1t 6419  eluzfz2t 6421  elfznnt 6426  elfz2nn0t 6427  elfznn0t 6428  fzss1t 6435  fzss2t 6436  elfzp1 6442  fzrev2t 6444  fzrev2it 6445  fzrev3t 6446  fsequb 6455  seqzeq 6487  seqzrn 6489  expgt1t 6523  recexpt 6526  expword2it 6536  expmwordit 6537  exple1t 6538  expubndt 6539  le2sqit 6563  bernneq 6583  expnbndt 6585  nn0opth 6596  sqrle 6637  sqrlt 6638  rpsqrclt 6645  sqr2irrlem1 6654  cru 6667  replimt 6692  crret 6702  crretOLD 6703  crimt 6704  crimtOLD 6705  recjt 6753  cj11t 6765  abs00 6777  absrpclt 6790  abslt 6810  absle 6811  absltOLD 6812  absleOLD 6813  nn0absclt 6816  lenegsqt 6823  abs2dift 6839  abs2difabst 6840  abs1m 6841  cvganz 6861  faclbnd 6882  faclbnd6 6891  permnnt 6911  fsum1ps 6956  fsumsplit 6958  fsumadd 6960  fsumshft 6969  fsumshftm 6970  fsumconst 6976  fsumabs2mul 6982  serzmulc 6996  binomlem5 7008  clm3 7017  clm4le 7019  climunii 7035  2climnn 7039  2climnn0 7040  climrecl 7047  climge0 7049  climaddlem3 7052  climaddc1 7054  climaddc2 7055  climmullem1 7056  climmullem2 7057  climmullem3 7058  climmullem4 7059  climmullem5 7060  climmullem8 7063  climsub 7066  climsubc2 7067  clim2serzt 7070  iserzmulc1 7072  climcmplem 7073  clim2serz 7081  climserzle 7083  climabslem 7084  climubi 7089  climcau 7092  caucvg3a 7100  caucvg3lem 7102  ser1f0 7106  iserzabslem 7114  cvgcmp2lem 7116  cvgcmp2clem 7118  cvgcmp 7120  cvgcmpub 7121  isum1p 7141  iserzgt0 7146  isummulc1ALT 7148  reccnv 7153  infcvglem2 7157  infcvglem3 7158  fnsmnt 7161  geolimilem 7170  georeclim 7175  geoisum1c 7180  cvgratlem1 7185  cvgratlem5 7189  fsum0diaglem2 7192  fsum0diag4 7196  elcncf1d 7205  mulc1cncf 7214  ivthlem7 7222  ivthlem7OLD 7231  efcltlem1 7246  efseq0ex 7253  erelem2 7262  erelem3 7263  efcj 7278  efaddlem2 7281  efaddlem5 7284  efaddlem6 7285  efaddlem9 7288  efaddlem10 7289  efaddlem17 7296  efaddlem27 7306  ef1tllem 7323  ef01tllem1 7325  absef01tllem 7328  eirrlem2 7331  eirrlem4 7333  abspef01tlub 7336  reeff1 7350  absefm1le 7352  efcn 7363  reeff1o 7368  sinclt 7373  cosclt 7374  efi4pt 7377  efieq 7392  sin01bndlem2 7410  sin01bndlem3 7411  cos01bndlem2 7412  cos01bndlem3 7413  sincos1sgn 7421  demoivre 7426  acdc2lem1 7430  acdc2lem2 7431  acdc5lem1 7433  acdclem 7436  znnen 7445  infpnlem2 7450  infxpidmlem7 7501  infxpidmlem10 7504  infxpidmlem11 7505  infxpidmlem12 7506  infmap2lem2 7522  infmap2 7523  eltopsp 7546  tpsex 7547  istps 7548  istps2 7549  tgclt 7566  tgss2t 7579  basgen2t 7581  subtop 7588  fctop 7592  cctop 7594  elcls 7646  neiss 7664  opnneissb 7669  opnssneib 7670  ssnei2 7671  innei 7677  neissex 7679  islp2 7688  clslp 7689  idcn 7705  cnco 7707  cnpco 7708  cnconst 7719  dnsconst 7727  ismsg 7739  ismsi 7740  ismeti 7741  metsym 7755  bl2in 7783  blcntr 7785  blss 7793  ssblex 7796  opnm 7800  opni3 7806  blssopn 7807  opntop 7810  blnei 7818  lpbl 7819  methausi 7820  metcnp 7826  tgioolem 7853  tgioo 7854  lmbr 7866  lmnn 7873  iscauf 7877  lmuni 7886  lmsslem 7887  lmfexlem3 7893  lmle 7895  metelcls 7900  metcnp4 7904  xplm 7909  xpcn 7910  lmcau 7930  cmsss 7931  bcthlem8 7940  bcthlem9 7941  bcthlem10 7942  bcthlem13 7945  bcthlem14 7946  bcthlem16 7948  bcthlem17 7949  bcthlem18 7950  bcthlem19 7951  bcthlem21 7953  bcthlem26 7958  bcthlem30 7962  isgrpi 7976  grpidinv 7986  grpideu 7987  isgrp2i 8011  ablmuldiv 8044  issubg 8053  ablmul 8068  ghgrpilem3 8072  cnring 8099  vcex 8137  isvc 8138  isvci 8139  nvex 8169  isnv 8170  nvpi 8233  nvabs 8240  nv1 8243  nmcnilem 8272  va1cnlem 8279  sm1cnilem 8281  sspval 8316  sspz 8328  nmoub3i 8368  nmblore 8378  0lno 8382  0blo 8384  nmlno0lem 8385  nmblolbii 8390  isblo3i 8392  blocnilem 8395  blocni 8396  sspph 8446  ipblnfi 8447  ubthlem3 8462  ubthlem4 8463  ubthlem9 8468  ubthlem10 8469  ubthlem11 8470  ubthlem12 8471  ubthlem13 8472  minveclem24 8499  minveclem25 8500  minveclem26 8501  minveclem27 8502  minveclem28 8503  minveclem30 8505  minveclem31 8506  minveclem32 8507  ssphl 8549  htthlem6 8555  htthlem8 8557  htthlem11 8560  psdmrn 8574  sincosq1sgn 8621  sinq12gt0t 8625  efifolem7 8643  efif1lem3 8647  circcltOLD 8656  shftefif1olem 8661  shftefif1olemOLD 8662  eff1i 8665  relogeftb 8687  bcsALT 8967  hlimunii 9029  hhsssh 9059  ocsh 9072  ocin 9085  occllem6 9094  occl 9097  projlem2 9103  projlem10 9111  projlem25 9126  projlem26 9127  projlem29 9130  pjthlem10 9143  pjtheu 9150  dfch2 9164  ococint 9212  shlub 9261  shslub 9273  shs00 9288  chj00 9325  spansnmul 9403  pjspansnt 9417  spanunsn 9419  fh1t 9478  fh2t 9479  cm2jt 9480  osumlem3 9497  5oalem1 9516  5oalem2 9517  5oalem4 9519  5oalem5 9520  3oalem2 9525  pjorth 9531  pjssm 9543  pjidt 9557  pjjs 9562  pjoi0t 9579  eigpos 9679  nmopret 9714  unopf1ot 9756  cnvunopt 9758  unoplint 9760  counopt 9761  hmopadj2t 9781  hmoplint 9782  bralnfnt 9788  eigvect 9802  eighmret 9803  eighmortht 9804  nmlnop0ALT 9835  lnopm 9840  lnophs 9841  nmopunt 9854  unopbdt 9855  hmopst 9860  hmopmt 9861  hmopcot 9863  nmcopexlem5 9870  nmophm 9876  bdophm 9877  lnopcon 9878  lncnopbd 9881  nmcfnexlem5 9899  lnfncon 9905  cnlnadjlem2 9916  cnlnadjlem7 9921  cnlnadjeu 9925  adjlnopt 9934  nmopcoadj 9948  branmfnt 9951  rnbra 9953  leoprf2t 9972  leopmulit 9978  leopmult 9979  leopnmidt 9982  nmopleidt 9983  pjnmop 9986  hmopidmch 9990  hmopidmpj 9991  pjhmopidm 10020  elpjcht 10026  pjin2 10031  pjclem4 10037  pj3s 10045  hstoct 10059  hstnmoct 10060  hstlet 10067  hstoht 10069  stles 10078  strlem3a 10089  strlem6 10093  hstrlem3a 10097  hstrlem6 10101  mdslj1 10154  mdslj2 10155  mdsl2b 10158  mdslmd1lem1 10160  mdslmd1lem2 10161  csmdsym 10169  mdexch 10170  h1dat 10184  atom1d 10188  shatomistic 10196  cvbr3 10202  atoml 10217  atcvatlem 10220  irredlem2 10226  atcvat3 10231  atcvat4 10232  mdsymlem2 10239  mdsymlem5 10242  mdsym 10246  sumdmdi 10249  cdj1 10265  cdj3 10273  lediv2itALT 10276  ghomid 10299  ghomf1olem 10301  cdrci 10381  truni1 10386  mapdiscn 10398  mapudiscn 10399  hmpher 10423  hmeogrp 10425  homcard 10426  qusp 10430  oefil2 10441  neifil 10442  filintf 10443  fgsb 10444  fgsb2 10449  efilcp2 10450  cnfilca 10451  t2t1 10460  mslb1 10473  2wsms 10474  msra3 10475  iintlem1 10476  iint 10478  trnij 10481  cnvtr 10482  aidm 10527  aidmold 10528  cmpmorp 10556  eqidob 10567  cmpassoh 10573  imonclem 10583  cmpmon 10585  idmon 10588  immon 10589

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 147  df-an 225

Copyright terms: Public domain