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 479  impbid 516  ordi 596  jcad 600  pm5.18 660  pm4.82 739  ecase2d 751  3jca 819  ecase23d 922  19.26 1067  19.40 1094  a4imed 1161  sb2 1177  sbequ1 1178  sbn 1231  eu2 1396  mooran2 1426  2eu1 1449  2eu3 1451  2eu6 1454  r19.40 1762  reu3 1931  reu6 1932  eqssd 2079  ssrabdv 2126  psstr 2150  ssin 2232  unineq 2255  un00 2306  raaan 2360  prss 2471  prel12 2484  preqsn 2486  opthwiener 2807  itlso 2863  unexb 2873  opeluu 2879  euuni 2881  reucl2 2888  rabsnt 2894  wereu 2945  elon2 2959  ordelord 2970  suceloni 3062  ordnbtwn 3063  dflim3 3118  ordom 3141  omssnlim 3145  opthprc 3221  xpsspw 3257  ideqg 3276  resiexg 3396  asymref2 3440  dminss 3462  imainss 3463  xpnz 3466  ssxpr 3475  relssdr 3513  dffun7 3540  funopg 3547  funun 3554  fununi 3563  fun11uni 3565  resfunexg 3579  fnco 3595  fnopabg 3615  fss 3635  fco 3636  funssxp 3638  ffdm 3639  f00 3657  dffo2 3675  fodmrnu 3680  foco 3682  f1o2 3693  f1f1orn 3699  f1ocnv 3701  f1o00 3714  fv3 3733  dff4 3816  dff2 3817  dffo4 3820  fopab2 3823  ffnfv 3828  fsn2 3836  fconstfv 3849  f1ocnvfv1 3878  f1ocnvfv2 3879  isocnv 3896  isotr 3897  isotrALT 3898  f1oiso 3904  tfrlem12 3922  fnoprabg 4012  2ndconst 4097  curry1 4098  1stcof 4101  eqop 4104  oalim 4167  omlim 4168  oelim 4169  oalimcl 4194  oaass 4195  omordi 4197  omlimcl 4209  oen0 4213  oeordi 4214  oewordri 4219  oeordsuc 4221  omsmo 4257  mapval2 4335  map0 4344  bren2 4389  en2d 4400  dom2d 4404  sbthlem9 4455  sdomex 4473  fodomr 4483  mapenlem2 4490  mapxpen 4495  xpmapenlem2 4497  xpmapenlem4 4499  xpmapenlem5 4500  mapunen 4502  php2 4514  php3 4515  php3OLD 4516  onomeneq 4519  omsdomnn 4530  unblem1 4540  unblem4 4543  unfilem1 4548  unifiOLD 4557  supmo 4576  supmax 4589  suppr 4590  supsnALT 4592  infensuc 4638  noinfep 4640  r1ord 4655  r1val1 4658  rankr1 4674  aceq3 4733  ac6lem 4754  fodom 4798  fodomb 4800  brdom3 4801  sucxpdom 4846  cardsdomel 4852  ondomon 4856  ondomcard 4857  carduni 4858  cardmin 4860  ltsopi 5016  addclpi 5020  mulclpi 5021  addcmpblnq 5052  addclpq 5058  addasspq 5063  distrpqlem 5066  distrpq 5067  1qec 5068  ltsopq 5075  ltexpq 5080  ltbtwnpq 5084  genpcl 5111  1pr 5117  prlem934 5139  ltexprlem5 5146  reclem2pr 5157  reclem3pr 5158  supexpr 5163  mulclsr 5193  mulasssr 5199  distrsr 5200  ltsosr 5203  recexsrlem 5212  suppsrlem 5221  suprelem 5259  axmulass 5278  axdistr 5279  ltxrltt 5500  ltso 5512  xrltso 5554  xrrebndt 5568  xrret 5569  mulnzcnopr 5702  divmuldivt 5780  divcan5t 5781  divadddivt 5784  conjmult 5797  ltmul12it 5841  lemul12it 5844  lemulge11t 5848  lediv1tOLD 5852  ltdiv2t 5887  ltrec1t 5888  lerec2t 5889  ledivdivt 5890  lediv2t 5891  lediv12it 5896  lediv2it 5897  recgt1it 5900  recp1lt1 5901  recrecltt 5902  ledivp1t 5905  nnleltp1t 5954  nndivtrt 5960  halfaddsubcl 6040  halfaddsubt 6041  lt2halvest 6042  lbinfm 6048  nnreclt 6072  xrsupsslem 6076  xrinfmsslem 6077  supxrunb1 6089  supxrunb2 6090  dfn2 6112  nn0ltp1let 6127  nn0addge1t 6130  nn0addge2t 6131  nnnegz 6138  elnnz 6145  elnnz1 6155  elnn0nn 6171  elnnnn0b 6173  elnnnn0c 6174  zltp1let 6181  z2get 6188  zextlet 6189  gtndivt 6193  msqznn 6196  peano2uz2 6201  uzind 6205  uzindOLD 6208  uzwo5OLD 6211  btwnz 6215  uzwo3lem1 6216  flidt 6235  flval2t 6238  flval3t 6239  flge0nn0t 6242  flge1nnt 6243  fladdzt 6244  quoremz 6251  quoremOLD 6252  intfracOLD 6254  intfracqOLD 6255  qret 6259  qnegclt 6270  qrecclt 6273  qbtwnre 6278  rpaddclt 6290  rpmulclt 6291  rpdivclt 6292  seq1rn 6322  shftf 6351  elioo4g 6385  eliooordt 6388  ioomax 6393  uzss 6431  eluzp1m1t 6433  eluzaddi 6436  eluzsubi 6437  uzind4 6450  elfz5t 6474  eluzfz1t 6487  eluzfz2t 6489  elfznnt 6494  elfz2nn0t 6495  elfznn0t 6496  fzss1t 6503  fzss2t 6504  elfzp1 6510  fzrev2t 6512  fzrev2it 6513  fzrev3t 6514  fsequb 6523  seqzeq 6555  seqzrn 6557  expgt1t 6592  recexpt 6595  expword2it 6605  expmwordit 6606  exple1t 6607  expubndt 6608  le2sqit 6632  bernneq 6652  expnbndt 6654  expnlbndt 6655  nn0opth 6666  sqrle 6707  sqrlt 6708  rpsqrclt 6715  sqr2irrlem1 6724  cru 6737  replimt 6761  crret 6769  crimt 6770  recjt 6818  cj11t 6830  abs00 6842  absrpclt 6855  abslt 6875  absle 6876  nn0absclt 6879  lenegsqt 6885  abs2dift 6902  abs2difabst 6903  abs1m 6904  cvganz 6924  faclbnd 6945  faclbnd6 6954  permnnt 6973  fsum1ps 7018  fsumsplit 7020  fsumadd 7022  fsumshft 7031  fsumshftm 7032  fsumconst 7038  fsumabs2mul 7044  serzmulc 7058  binomlem5 7070  clm3 7079  clm4le 7081  climunii 7098  2climnn 7102  2climnn0 7103  climrecl 7110  climge0 7112  climaddlem3 7116  climaddc1 7118  climaddc2 7119  climmullem1 7120  climmullem2 7121  climmullem3 7122  climmullem4 7123  climmullem5 7124  climmullem8 7127  climsub 7130  climsubc2 7131  clim2serzt 7134  iserzmulc1 7136  climcmplem 7137  clim2serz 7145  climserzle 7147  climabslem 7148  climubi 7153  climcau 7156  caucvg3a 7164  caucvg3lem 7166  ser1f0 7170  iserzabslem 7178  cvgcmp2lem 7180  cvgcmp2clem 7182  cvgcmp 7184  cvgcmpub 7185  isum1p 7206  iserzgt0 7211  isummulc1ALT 7213  reccnv 7218  infcvglem2 7222  infcvglem3 7223  fnsmnt 7226  geolimilem 7235  georeclim 7240  geoisum1c 7245  cvgratlem1 7250  cvgratlem5 7254  fsum0diaglem2 7257  fsum0diag4 7261  elcncf1d 7270  mulc1cncf 7279  ivthlem7 7287  efcltlem1 7304  efseq0ex 7311  erelem2 7320  erelem3 7321  efcj 7336  efaddlem2 7339  efaddlem5 7342  efaddlem6 7343  efaddlem9 7346  efaddlem10 7347  efaddlem17 7354  efaddlem27 7364  ef1tllem 7381  ef01tllem1 7383  absef01tllem 7387  eirrlem2 7390  eirrlem4 7392  abspef01tlub 7395  reeff1 7410  absefm1le 7412  efcn 7423  reeff1o 7426  sinclt 7431  cosclt 7432  efi4pt 7435  efieq 7450  sin01bndlem2 7468  sin01bndlem3 7469  cos01bndlem2 7470  cos01bndlem3 7471  sincos1sgn 7479  demoivre 7484  acdc2lem1 7488  acdc2lem2 7489  acdc5lem1 7491  acdclem 7494  znnen 7502  infpnlem2 7507  infxpidmlem7 7558  infxpidmlem10 7561  infxpidmlem11 7562  infxpidmlem12 7563  infmap2lem2 7580  infmap2 7581  eltopsp 7604  tpsex 7605  istps 7606  istps2 7607  tgclt 7624  tgss2t 7637  basgen2t 7639  subtop 7646  fctopOLD 7650  cctop 7652  elcls 7704  neiss 7723  opnneissb 7728  opnssneib 7729  ssnei2 7730  innei 7736  neissex 7738  islp2 7747  clslp 7748  idcn 7766  cnco 7768  cnpco 7769  cnconst 7780  dnsconst 7788  ismsg 7800  ismsi 7801  ismeti 7802  metsym 7816  bl2in 7843  blcntr 7845  blss 7853  ssblex 7856  opnm 7860  opni3 7866  blssopn 7867  opntop 7870  blnei 7879  lpbl 7880  methausi 7881  metcnp 7887  tgioolem 7914  tgioo 7915  lmbr 7928  lmnn 7935  iscauf 7939  lmuni 7951  lmsslem 7952  lmfexlem3 7958  lmle 7960  metelcls 7965  metcnp4 7970  xplm 7975  xpcn 7976  lmcau 7996  cmsss 7997  bcthlem8 8006  bcthlem9 8007  bcthlem10 8008  bcthlem13 8011  bcthlem14 8012  bcthlem16 8014  bcthlem17 8015  bcthlem18 8016  bcthlem19 8017  bcthlem21 8019  bcthlem26 8024  bcthlem30 8028  isgrpi 8042  grpidinv 8052  grpideu 8053  isgrp2i 8076  ablmuldiv 8107  issubg 8116  ablmul 8131  ghgrpilem3 8135  cnring 8162  vcex 8199  isvc 8200  isvci 8201  nvex 8230  isnv 8231  nvpi 8294  nvabs 8301  nv1 8304  nmcnilem 8337  va1cnlem 8345  sm1cnilem 8347  sspval 8382  sspz 8394  nmoub3i 8436  nmblore 8446  0lno 8450  0blo 8452  nmlno0lem 8453  nmblolbii 8459  isblo3i 8461  blocnilem 8464  blocni 8465  sspph 8515  ipblnfi 8516  ubthlem3 8531  ubthlem4 8532  ubthlem9 8537  ubthlem10 8538  ubthlem11 8539  ubthlem12 8540  ubthlem13 8541  minveclem24 8568  minveclem25 8569  minveclem26 8570  minveclem27 8571  minveclem28 8572  minveclem30 8574  minveclem31 8575  minveclem32 8576  ssphl 8619  htthlem6 8625  htthlem8 8627  htthlem11 8630  psdmrn 8648  spwpr3OLD 8662  sincosq1sgn 8704  sinq12gt0t 8708  sineq0 8713  efifolem7 8728  efif1lem3 8732  shftefif1olem 8741  eff1i 8744  relogeftb 8765  bcsALT 9046  hlimunii 9108  hhsssh 9139  ocsh 9156  ocin 9169  occllem6 9178  occl 9181  projlem2 9187  projlem10 9195  projlem25 9210  projlem26 9211  projlem29 9214  pjthlem10 9228  pjtheu 9235  dfch2 9249  ococint 9297  shlub 9346  shslub 9358  shs00 9373  chj00 9410  spansnmul 9487  pjspansnt 9500  spanunsn 9502  fh1t 9561  fh2t 9562  cm2jt 9563  osumlem3 9580  5oalem1 9599  5oalem2 9600  5oalem4 9602  5oalem5 9603  3oalem2 9608  pjorth 9614  pjssm 9626  pjidt 9640  pjjs 9645  pjoi0t 9662  eigpos 9762  nmopret 9797  unopf1ot 9840  cnvunopt 9842  unoplint 9844  counopt 9845  hmopadj2t 9865  hmoplint 9866  bralnfnt 9872  eigvect 9886  eighmret 9887  eighmortht 9888  nmlnop0ALT 9920  lnopm 9925  lnophs 9926  nmopunt 9939  unopbdt 9940  hmopst 9945  hmopmt 9946  hmopcot 9948  nmcopexlem5 9955  nmophm 9961  bdophm 9962  lnopcon 9963  lncnopbd 9966  nmcfnexlem5 9984  lnfncon 9990  cnlnadjlem2 10001  cnlnadjlem7 10006  cnlnadjeu 10010  adjlnopt 10019  nmopcoadj 10034  branmfnt 10038  rnbra 10040  leoprf2t 10060  leopmulit 10066  leopmult 10067  leopnmidt 10071  nmopleidt 10072  pjnmop 10075  hmopidmch 10079  hmopidmpj 10080  pjhmopidm 10110  elpjcht 10116  pjin2 10121  pjclem4 10127  pj3s 10135  hstoct 10149  hstnmoct 10150  hstlet 10157  hstoht 10159  stles 10168  strlem3a 10179  strlem6 10183  hstrlem3a 10187  hstrlem6 10191  dmdbr5 10235  mdslj1 10246  mdslj2 10247  mdsl2b 10250  mdslmd1lem1 10252  mdslmd1lem2 10253  csmdsym 10261  mdexch 10262  h1dat 10276  atom1d 10280  shatomistic 10288  cvbr3 10294  atoml 10309  atcvatlem 10312  irredlem2 10318  atcvat3 10323  atcvat4 10324  mdsymlem2 10331  mdsymlem5 10334  mdsym 10338  sumdmdi 10342  cdj1 10360  cdj3 10368  lediv2itALT 10371  ghomid 10394  ghomf1olem 10396  nndivlub 10422  cdrci 10494  truni1 10499  mapdiscn 10511  mapudiscn 10512  hmpher 10536  hmeogrp 10538  homcard 10539  hmeobc 10542  homindlem2 10550  homindlem3 10551  qusp 10555  oefil2 10567  neifil 10568  filintf 10569  fgsb 10570  fgsbOLD 10571  fgsb2 10580  efilcp2 10581  efilcp2OLD 10582  cnfilca 10583  cnfilcaOLD 10584  rcfpfillem3 10589  rcfpfillem3OLD 10590  rcfpfil 10597  rcfpfilOLD 10598  sfvlim 10605  t2t1 10616  mslb1 10629  2wsms 10630  msra3 10631  iintlem1 10632  iint 10634  trnij 10637  cnvtr 10638  aidm 10683  aidmold 10684  cmpmorp 10712  eqidob 10723  cmpassoh 10729  imonclem 10741  cmpmon 10743  idmon 10745  immon 10746  idfisf 10760

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