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 424  pm4.43 433  ancom 437  syl2anc 474  abai 481  impbid 518  ordi 598  jcad 602  pm5.18 662  pm4.82 741  ecase2d 753  3jca 821  ecase23d 924  19.26 1069  19.40 1096  a4imed 1163  sb2 1179  sbequ1 1180  sbn 1233  eu2 1398  mooran2 1428  2eu1 1452  2eu3 1454  2eu6 1457  r19.40 1765  reu3 1934  reu6 1935  eqssd 2083  ssrabdv 2130  psstr 2154  ssin 2236  unineq 2259  un00 2311  raaan 2365  prss 2476  prel12 2489  preqsn 2491  opthwiener 2814  itlso 2870  unexb 2880  opeluu 2886  euuni 2888  reucl2 2895  rabsnt 2901  wereu 2952  elon2 2966  ordelord 2977  suceloni 3069  ordnbtwn 3070  dflim3 3125  ordom 3148  omssnlim 3152  opthprc 3228  xpsspw 3264  ideqg 3283  resiexg 3403  asymref2 3447  dminss 3469  imainss 3470  xpnz 3473  ssxpr 3482  relssdr 3520  dffun7 3547  funopg 3554  funun 3561  fununi 3570  fun11uni 3572  resfunexg 3586  fnco 3602  fnopabg 3622  fss 3642  fco 3643  funssxp 3645  ffdm 3646  f00 3664  dffo2 3682  fodmrnu 3687  foco 3689  f1o2 3700  f1f1orn 3706  f1ocnv 3708  f1o00 3721  fv3 3740  dff4 3823  dff2 3824  dffo4 3827  fopab2 3830  ffnfv 3835  fsn2 3843  fconstfv 3856  f1ocnvfv1 3885  f1ocnvfv2 3886  isocnv 3903  isotr 3904  isotrALT 3905  f1oiso 3911  tfrlem12 3929  fnoprabg 4019  2ndconst 4104  curry1 4105  1stcof 4108  eqop 4111  oalim 4174  omlim 4175  oelim 4176  oalimcl 4201  oaass 4202  omordi 4204  omlimcl 4216  oen0 4220  oeordi 4221  oewordri 4226  oeordsuc 4228  omsmo 4264  mapval2 4342  map0 4351  bren2 4396  en2d 4407  dom2d 4411  sbthlem9 4462  sdomex 4480  fodomr 4490  mapenlem2 4497  mapxpen 4502  xpmapenlem2 4504  xpmapenlem4 4506  xpmapenlem5 4507  mapunen 4509  php2 4521  php3 4522  php3OLD 4523  onomeneq 4526  omsdomnn 4540  unblem1 4553  unblem4 4556  unfilem1 4562  unifi 4572  unifiOLD 4574  supmo 4592  supmax 4605  suppr 4606  supsnALT 4608  infensuc 4655  noinfep 4657  r1ord 4672  r1val1 4675  rankr1 4691  aceq3 4750  ac6lem 4771  fodom 4815  fodomb 4817  brdom3 4818  sucxpdom 4864  cardsdomel 4870  ondomon 4874  ondomcard 4875  carduni 4876  cardmin 4878  ltsopi 5035  addclpi 5039  mulclpi 5040  addcmpblnq 5071  addclpq 5077  addasspq 5082  distrpqlem 5085  distrpq 5086  1qec 5087  ltsopq 5094  ltexpq 5099  ltbtwnpq 5103  genpcl 5130  1pr 5136  prlem934 5158  ltexprlem5 5165  reclem2pr 5176  reclem3pr 5177  supexpr 5182  mulclsr 5212  mulasssr 5218  distrsr 5219  ltsosr 5222  recexsrlem 5231  suppsrlem 5240  suprelem 5278  axmulass 5297  axdistr 5298  ltxrltt 5519  ltso 5531  xrltso 5573  xrrebndt 5587  xrret 5588  mulnzcnopr 5721  divmuldivt 5789  divcan5t 5790  divadddivt 5793  conjmult 5806  ltmul12it 5850  lemul12it 5853  lemulge11t 5857  lediv1tOLD 5861  ltdiv2t 5896  ltrec1t 5897  lerec2t 5898  ledivdivt 5899  lediv2t 5900  lediv12it 5905  lediv2it 5906  recgt1it 5909  recp1lt1 5910  recrecltt 5911  ledivp1t 5914  nnleltp1t 5963  nndivtrt 5969  halfaddsubcl 6049  halfaddsubt 6050  lt2halvest 6051  lbinfm 6057  nnreclt 6081  xrsupsslem 6085  xrinfmsslem 6086  supxrunb1 6098  supxrunb2 6099  dfn2 6121  nn0ltp1let 6136  nn0addge1t 6139  nn0addge2t 6140  nnnegz 6147  elnnz 6154  elnnz1 6164  elnn0nn 6180  elnnnn0b 6182  elnnnn0c 6183  zltp1let 6190  z2get 6197  zextlet 6198  gtndivt 6202  msqznn 6205  peano2uz2 6210  uzind 6214  uzindOLD 6217  uzwo5OLD 6220  btwnz 6224  uzwo3lem1 6225  flidt 6244  flval2t 6247  flval3t 6248  flge0nn0t 6251  flge1nnt 6252  fladdzt 6253  quoremz 6260  intfracq 6262  fldivt 6263  qret 6267  qnegclt 6278  qrecclt 6281  qbtwnre 6286  rpaddclt 6298  rpmulclt 6299  rpdivclt 6300  seq1rn 6330  shftf 6359  elioo4g 6393  eliooordt 6396  ioomax 6401  uzss 6439  eluzp1m1t 6441  eluzaddi 6444  eluzsubi 6445  uzind4 6458  elfz5t 6482  eluzfz1t 6495  eluzfz2t 6497  elfznnt 6502  elfz2nn0t 6503  elfznn0t 6504  fzss1t 6511  fzss2t 6512  elfzp1 6518  fzrev2t 6520  fzrev2it 6521  fzrev3t 6522  fsequb 6531  seqzeq 6563  seqzrn 6565  expgt1t 6600  recexpt 6603  expword2it 6613  expmwordit 6614  exple1t 6615  expubndt 6616  le2sqit 6640  bernneq 6660  expnbndt 6662  expnlbndt 6663  nn0opth 6674  sqrle 6715  sqrlt 6716  rpsqrclt 6723  sqr2irrlem1 6732  cru 6745  replimt 6769  crret 6777  crimt 6778  recjt 6825  cj11t 6837  abs00 6849  absrpclt 6862  abslt 6882  absle 6883  nn0absclt 6886  lenegsqt 6892  abs2dift 6909  abs2difabst 6910  abs1m 6911  cvganz 6931  faclbnd 6952  faclbnd6 6961  permnnt 6980  fsum1ps 7025  fsumsplit 7027  fsumadd 7029  fsumshft 7038  fsumshftm 7039  fsumconst 7045  fsumabs2mul 7051  serzmulc 7065  binomlem5 7077  clm3 7086  clm4le 7088  climunii 7105  2climnn 7109  2climnn0 7110  climrecl 7117  climge0 7119  climaddlem3 7123  climaddc1 7125  climaddc2 7126  climmullem1 7127  climmullem2 7128  climmullem3 7129  climmullem4 7130  climmullem5 7131  climmullem8 7134  climsub 7137  climsubc2 7138  clim2serzt 7141  iserzmulc1 7143  climcmplem 7144  clim2serz 7152  climserzle 7154  climabslem 7155  climubi 7160  climcau 7163  caucvg3a 7171  caucvg3lem 7173  ser1f0 7177  iserzabslem 7185  cvgcmp2lem 7187  cvgcmp2clem 7189  cvgcmp 7191  cvgcmpub 7192  isum1p 7213  iserzgt0 7218  isummulc1ALT 7220  reccnv 7225  infcvglem2 7229  infcvglem3 7230  fnsmnt 7233  geolimilem 7242  georeclim 7247  geoisum1c 7252  cvgratlem1 7257  cvgratlem5 7261  fsum0diaglem2 7264  fsum0diag4 7268  elcncf1d 7277  mulc1cncf 7286  ivthlem7 7294  efcltlem1 7311  efseq0ex 7318  erelem2 7327  erelem3 7328  efcj 7343  efaddlem2 7346  efaddlem5 7349  efaddlem6 7350  efaddlem9 7353  efaddlem10 7354  efaddlem17 7361  efaddlem27 7371  ef1tllem 7388  ef01tllem1 7390  absef01tllem 7394  eirrlem2 7397  eirrlem4 7399  abspef01tlub 7402  reeff1 7417  absefm1le 7419  efcn 7430  reeff1o 7433  sinclt 7438  cosclt 7439  efi4pt 7442  efieq 7457  sin01bndlem2 7476  sin01bndlem3 7477  cos01bndlem2 7478  cos01bndlem3 7479  sincos1sgn 7487  demoivre 7492  acdc2lem1 7496  acdc2lem2 7497  acdc5lem1 7499  acdclem 7502  znnen 7510  infpnlem2 7515  infxpidmlem7 7566  infxpidmlem10 7569  infxpidmlem11 7570  infxpidmlem12 7571  infmap2lem2 7589  infmap2 7590  eltopsp 7612  tpsex 7613  istps 7614  istps2 7615  tgclt 7630  tgss2t 7643  basgen2t 7645  subtop 7650  fctopOLD 7654  cctop 7656  elcls 7708  neiss 7727  opnneissb 7732  opnssneib 7733  ssnei2 7734  innei 7740  neissex 7742  islp2 7751  clslp 7752  idcn 7770  cnco 7772  cnpco 7773  cnconst 7784  dnsconst 7792  ismsg 7804  ismsi 7805  ismeti 7806  metsym 7820  bl2in 7847  blcntr 7849  blss 7857  ssblex 7860  opnm 7864  opni3 7870  blssopn 7871  opntop 7874  blnei 7883  lpbl 7884  methausi 7885  metcnp 7891  tgioolem 7918  tgioo 7919  lmbr 7932  lmnn 7939  iscauf 7943  lmuni 7955  lmsslem 7956  lmfexlem3 7962  lmle 7964  metelcls 7969  metcnp4 7974  xplm 7979  xpcn 7980  lmcau 8000  cmsss 8001  bcthlem8 8010  bcthlem9 8011  bcthlem10 8012  bcthlem13 8015  bcthlem14 8016  bcthlem16 8018  bcthlem17 8019  bcthlem18 8020  bcthlem19 8021  bcthlem21 8023  bcthlem26 8028  bcthlem30 8032  isgrpi 8046  grpidinv 8056  grpideu 8057  isgrp2i 8079  ablmuldiv 8110  issubg 8119  ablmul 8134  ghgrpilem3 8138  cnring 8165  vcex 8202  isvc 8203  isvci 8204  nvex 8233  isnv 8234  nvpi 8297  nvabs 8304  nv1 8307  nmcnilem 8340  va1cnlem 8348  sm1cnilem 8350  sspval 8385  sspz 8397  nmoub3i 8439  nmblore 8449  0lno 8453  0blo 8455  nmlno0lem 8456  nmblolbii 8462  isblo3i 8464  blocnilem 8467  blocni 8468  sspph 8518  ipblnfi 8519  ubthlem3 8534  ubthlem4 8535  ubthlem9 8540  ubthlem10 8541  ubthlem11 8542  ubthlem12 8543  ubthlem13 8544  minveclem24 8571  minveclem25 8572  minveclem26 8573  minveclem27 8574  minveclem28 8575  minveclem30 8577  minveclem31 8578  minveclem32 8579  ssphl 8622  htthlem6 8628  htthlem8 8630  htthlem11 8633  psdmrn 8651  sincosq1sgn 8706  sinq12gt0t 8710  sineq0 8715  efifolem7 8730  efif1lem3 8734  shftefif1olem 8743  eff1i 8746  relogeftb 8767  bcsALT 9048  hlimunii 9110  hhsssh 9141  ocsh 9158  ocin 9171  occllem6 9180  occl 9183  projlem2 9189  projlem10 9197  projlem25 9212  projlem26 9213  projlem29 9216  pjthlem10 9230  pjtheu 9237  dfch2 9251  ococint 9299  shlub 9348  shslub 9360  shs00 9375  chj00 9412  spansnmul 9489  pjspansnt 9502  spanunsn 9504  fh1t 9563  fh2t 9564  cm2jt 9565  osumlem3 9582  5oalem1 9601  5oalem2 9602  5oalem4 9604  5oalem5 9605  3oalem2 9610  pjorth 9616  pjssm 9628  pjidt 9642  pjjs 9647  pjoi0t 9664  eigpos 9764  nmopret 9799  unopf1ot 9842  cnvunopt 9844  unoplint 9846  counopt 9847  hmopadj2t 9867  hmoplint 9868  bralnfnt 9874  eigvect 9888  eighmret 9889  eighmortht 9890  nmlnop0ALT 9922  lnopm 9927  lnophs 9928  nmopunt 9941  unopbdt 9942  hmopst 9947  hmopmt 9948  hmopcot 9950  nmcopexlem5 9957  nmophm 9963  bdophm 9964  lnopcon 9965  lncnopbd 9968  nmcfnexlem5 9986  lnfncon 9992  cnlnadjlem2 10003  cnlnadjlem7 10008  cnlnadjeu 10012  adjlnopt 10021  nmopcoadj 10036  branmfnt 10040  rnbra 10042  leoprf2t 10062  leopmulit 10068  leopmult 10069  leopnmidt 10073  nmopleidt 10074  pjnmop 10077  hmopidmch 10081  hmopidmpj 10082  pjhmopidm 10112  elpjcht 10119  pjin2 10124  pjclem4 10130  pj3s 10138  hstoct 10152  hstnmoct 10153  hstlet 10160  hstoht 10162  stles 10171  strlem3a 10182  strlem6 10186  hstrlem3a 10190  hstrlem6 10194  dmdbr5 10238  mdslj1 10249  mdslj2 10250  mdsl2b 10253  mdslmd1lem1 10255  mdslmd1lem2 10256  csmdsym 10264  mdexch 10265  h1dat 10279  atom1d 10283  shatomistic 10291  cvbr3 10297  atoml 10312  atcvatlem 10315  irredlem2 10321  atcvat3 10326  atcvat4 10327  mdsymlem2 10334  mdsymlem5 10337  mdsym 10341  sumdmdi 10345  cdj1 10363  cdj3 10371  lediv2itALT 10374  ghomid 10397  ghomf1olem 10399  nndivlub 10425  inposet 10485  cdrci 10488  truni1 10493  mapdiscn 10505  mapudiscn 10506  hmpher 10530  hmeogrp 10532  homcard 10533  hmeobc 10536  homindlem3 10545  qusp 10549  oefil2 10560  neifil 10561  filintf 10562  fgsb 10563  fgsb2 10568  efilcp2 10569  cnfilca 10570  rcfpfillem3 10573  rcfpfil 10577  sfvlim 10584  t2t1 10595  mslb1 10608  2wsms 10609  msra3 10610  iintlem1 10611  iint 10613  trnij 10616  cnvtr 10617  aidm 10662  cmpmorp 10691  eqidob 10702  cmpassoh 10708  imonclem 10720  cmpmon 10722  idmon 10724  immon 10725  idfisf 10739

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