ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  jca Unicode version

Theorem jca 304
Description: Deduce conjunction of the consequents of two implications ("join consequents with 'and'"). (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)
Hypotheses
Ref Expression
jca.1  |-  ( ph  ->  ps )
jca.2  |-  ( ph  ->  ch )
Assertion
Ref Expression
jca  |-  ( ph  ->  ( ps  /\  ch ) )

Proof of Theorem jca
StepHypRef Expression
1 jca.1 . 2  |-  ( ph  ->  ps )
2 jca.2 . 2  |-  ( ph  ->  ch )
3 pm3.2 138 . 2  |-  ( ps 
->  ( ch  ->  ( ps  /\  ch ) ) )
41, 2, 3sylc 62 1  |-  ( ph  ->  ( ps  /\  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107
This theorem is referenced by:  jca31  307  jca32  308  jcai  309  jctil  310  jctir  311  ancli  321  ancri  322  sylanbrc  414  jcab  593  ioran  742  ordi  806  stdcndc  831  stdcndcOLD  832  dfandc  870  pm4.55dc  923  mpbi2and  928  mpbir2and  929  pm4.82  935  pm4.83dc  936  rnlem  961  syl22anc  1218  syl112anc  1221  syl121anc  1222  syl211anc  1223  syl23anc  1224  syl32anc  1225  syl122anc  1226  syl212anc  1227  syl221anc  1228  syl222anc  1233  syl123anc  1234  syl132anc  1235  syl213anc  1236  syl231anc  1237  syl312anc  1238  syl321anc  1239  syl223anc  1243  syl232anc  1244  syl322anc  1245  syl233anc  1246  syl323anc  1247  syl332anc  1248  ecased  1328  19.26  1458  nfand  1548  19.40  1611  equsexd  1708  sbcof2  1783  sbequ8  1820  eu2  2044  eu3h  2045  eu5  2047  mooran2  2073  datisi  2110  felapton  2114  darapti  2115  dimatis  2117  fresison  2118  fesapo  2120  reximssdv  2539  r19.26  2561  r19.29af2  2575  r19.40  2588  eqvinc  2811  eqvincg  2812  elrabd  2845  reu6  2876  reu3  2877  indifdir  3336  undif3ss  3341  un00  3413  eqifdc  3510  disjpr2  3594  prel12  3705  prneimg  3708  preqsn  3709  disjiun  3931  opth  4166  0nelop  4177  euotd  4183  opelopabsb  4189  ispod  4233  elon2  4305  unexb  4370  opeluu  4378  eusvnfb  4382  suc11g  4479  nlimsucg  4488  tfi  4503  vtoclr  4594  opthprc  4597  ideqg  4697  resiexg  4871  dminss  4960  imainss  4961  ssxpbm  4981  relrelss  5072  funopg  5164  fntpg  5186  fun11uni  5200  imain  5212  funimaexglem  5213  funssxp  5299  ffdm  5300  f00  5321  dffo2  5356  fodmrnu  5360  foco  5362  fun11iun  5395  f1o00  5409  fsnd  5417  fv3  5451  dff2  5571  dff3im  5572  dffo4  5575  ffnfv  5585  ffvresb  5590  fsn2  5601  fconstfvm  5645  fnfvima  5659  fcof1o  5697  isocnv  5719  isotr  5724  riotaprop  5760  acexmidlemcase  5776  caovlem2d  5970  f1ocnvd  5979  caofcom  6012  resfunexgALT  6015  elxp7  6075  2ndrn  6088  1stconst  6125  2ndconst  6126  cnvf1olem  6128  poxp  6136  dftpos4  6167  dfsmo2  6191  tfrlem5  6218  tfrlemiex  6235  tfr1onlemsucaccv  6245  tfr1onlembfn  6248  tfr1onlemex  6251  tfr1onlemres  6253  tfrcllemsucaccv  6258  tfrcllembfn  6261  tfrcllemex  6264  tfrcllemres  6266  tfrcl  6268  frecabex  6302  frecabcl  6303  frecfcllem  6308  frecrdg  6312  oawordi  6372  nntri3  6400  nntr2  6406  nnmordi  6419  iserd  6462  relelec  6476  erth  6480  qliftfun  6518  mapsncnv  6596  mptelixpg  6635  bren  6648  findcard2d  6792  findcard2sd  6793  isinfinf  6798  tridc  6800  nnwetri  6811  undifdcss  6818  fiintim  6824  fisseneq  6827  fidcenumlemim  6847  sbthlemi9  6860  supisolem  6902  ordiso2  6927  updjud  6974  difinfsn  6992  ctssdccl  7003  omniwomnimkv  7048  acfun  7079  ccfunen  7095  cc4f  7100  cc4n  7102  elni2  7145  dfplpq2  7185  dfmpq2  7186  enqbreq2  7188  enqdc1  7193  addcmpblnq  7198  addclnq  7206  nqpi  7209  addassnqg  7213  mulassnqg  7215  mulcanenq  7216  distrnqg  7218  1qec  7219  recexnq  7221  subhalfnqq  7245  enq0tr  7265  nqnq0pi  7269  nq0nn  7273  mulcanenq0ec  7276  nnnq0lem1  7277  addclnq0  7282  distrnq0  7290  addassnq0lemcl  7292  elnp1st2nd  7307  prarloc  7334  addlocprlemlt  7362  addlocprlemeq  7364  addlocprlemgt  7365  addclpr  7368  nqprm  7373  mullocprlem  7401  mullocpr  7402  mulclpr  7403  ltpopr  7426  ltaddpr  7428  ltexprlemm  7431  ltexprlemopl  7432  ltexprlemopu  7434  ltexprlemrnd  7436  ltexprlemdisj  7437  addcanprleml  7445  addcanprlemu  7446  addcanprg  7447  recexprlemm  7455  recexprlemopl  7456  recexprlemopu  7458  recexprlemrnd  7460  recexprlemdisj  7461  cauappcvgprlemm  7476  cauappcvgprlemopl  7477  cauappcvgprlemopu  7479  cauappcvgprlemrnd  7481  cauappcvgprlemdisj  7482  cauappcvgprlemlim  7492  caucvgprlemnkj  7497  caucvgprlemm  7499  caucvgprlemopl  7500  caucvgprlemopu  7502  caucvgprlemrnd  7504  caucvgprlemlim  7512  caucvgprprlemnkltj  7520  caucvgprprlemnkeqj  7521  caucvgprprlemnjltk  7522  caucvgprprlemm  7527  caucvgprprlemopl  7528  caucvgprprlemopu  7530  caucvgprprlemrnd  7532  caucvgprprlemexbt  7537  caucvgprprlemlim  7542  suplocexprlemrl  7548  suplocexprlemru  7550  suplocexprlemdisj  7551  suplocexprlemloc  7552  suplocexprlemex  7553  suplocexprlemub  7554  prsrlem1  7573  mulclsr  7585  mulasssrg  7589  distrsrg  7590  suplocsrlemb  7637  elreal2  7661  axmulass  7704  axdistr  7705  axcaucvglemcau  7729  add20  8259  mullt0  8265  rereim  8371  ltmul1  8377  cru  8387  mulap0r  8400  aprcl  8431  divmuldivap  8495  divmuleqap  8500  divadddivap  8510  divmuldivapd  8615  div2subap  8619  ltmul12a  8641  lemul12a  8643  lemulge11  8647  lediv12a  8675  lediv2a  8676  recgt1i  8679  recreclt  8681  ledivp1  8684  lemul1ad  8720  lemul2ad  8721  ltmul12ad  8722  lemul12ad  8723  lemul12bd  8724  nndivre  8779  nndivtr  8785  halfaddsubcl  8976  halfaddsub  8977  lt2halves  8978  nnrecl  8998  elnn0nn  9042  elnnnn0b  9044  elnnnn0c  9045  nn0addge1  9046  nn0addge2  9047  xnn0xrnemnf  9075  elnn0z  9090  elnnz1  9100  nzadd  9129  elz2  9145  zdivadd  9163  zdivmul  9164  zextle  9165  peano2uz2  9181  uzind  9185  btwnz  9193  uzss  9369  eluzp1m1  9372  eluz2b2  9423  qre  9443  qaddcl  9453  qmulcl  9455  qreccl  9460  irradd  9464  irrmul  9465  elpqb  9467  cnref1o  9468  rprege0  9484  rprene0  9487  rpreap0  9488  rpcnne0  9489  rpcnap0  9490  rpregt0d  9519  rprege0d  9520  rprene0d  9521  rpcnne0d  9522  lediv2ad  9535  ledivge1le  9542  lediv12ad  9572  nnledivrp  9582  nn0ledivnn  9583  xrlttri3  9612  xrrebnd  9631  xrrege0  9637  xnn0xadd0  9679  xlesubadd  9695  elioo4g  9746  ioomax  9760  iccmax  9761  divelunit  9814  elfz5  9828  uzsubsubfz  9857  fzopth  9871  fzass4  9872  fzrev2  9895  uzsplit  9902  elfz2nn0  9922  difelfzle  9941  1fv  9946  4fvwrd4  9947  fzo1fzo0n0  9990  elfzom1elp1fzo  10009  subfzo0  10049  qtri3or  10050  adddivflid  10095  flltdivnn0lt  10107  intfracq  10123  modqid2  10154  modfzo0difsn  10198  seq3val  10261  seqvalcd  10262  iseqf1olemqcl  10289  iseqf1olemnab  10291  iseqf1olemab  10292  iseqf1olemmo  10295  seq3f1olemqsumkj  10301  seq3f1olemqsumk  10302  expclzaplem  10347  leexp1a  10378  expubnd  10380  le2sq2  10398  sumsqeq0  10401  bernneq  10442  expnlbnd  10446  nn0opthd  10499  faclbnd6  10521  facavg  10523  seq3coll  10616  shftlem  10619  shftfvalg  10621  shftfval  10624  cvg1nlemcau  10787  cvg1nlemres  10788  rexuz3  10793  resqrexlemcvg  10822  resqrexlemglsq  10825  resqrexlemga  10826  sqrtle  10839  sqrtlt  10840  sqrt11  10842  sqrtsq2  10846  absmul  10872  sqabs  10885  abslt  10891  absle  10892  lenegsq  10898  maxleastb  11017  maxltsup  11021  rexanre  11023  negfi  11030  xrmaxiflemab  11047  xrmaxiflemlub  11048  xrmaxltsup  11058  xrmaxadd  11061  climcn2  11109  mulcn2  11112  summodclem2a  11181  summodc  11183  fsum3  11187  fsum3cvg3  11196  fsumcl2lem  11198  fsumadd  11206  fsump1i  11233  fsum0diaglem  11240  mptfzshft  11242  fsumrev  11243  fsummulc2  11248  fsum00  11262  expcnvap0  11302  mertenslemi1  11335  ntrivcvgap0  11349  prodmodclem3  11375  prodmodclem2a  11376  zproddc  11379  eftlub  11431  efieq  11476  sincos1sgn  11505  demoivreALT  11514  dvdsval3  11531  dvdscmul  11554  dvdsmulc  11555  dvdscmulr  11556  dvdsmulcr  11557  modmulconst  11559  dvds2ln  11560  ltoddhalfle  11624  nn0o  11638  divalg2  11657  ndvdssub  11661  ndvdsadd  11662  infssuzex  11676  divgcdz  11694  gcd0id  11701  gcdaddm  11706  bezoutlemstep  11719  bezoutlemmain  11720  dfgcd3  11732  dfgcd2  11736  lcmcllem  11782  dvdslcm  11784  lcmgcdlem  11792  lcmgcdnn  11797  qredeq  11811  qredeu  11812  rpdvds  11814  divgcdcoprm0  11816  cncongr1  11818  cncongr2  11819  cncongrcoprm  11821  prmind2  11835  isprm6  11859  prmexpb  11863  cncongrprm  11869  sqrt2irrlem  11873  pw2dvdslemn  11877  oddpwdclemxy  11881  oddpwdclemdc  11885  oddpwdc  11886  hashdvds  11931  hashgcdlem  11937  ennnfonelemfun  11964  ennnfonelemim  11971  ctinfomlemom  11974  ctinfom  11975  ctinf  11977  ctiunctlemfo  11986  omctfn  11990  topgele  12233  tgcl  12270  epttop  12296  opnssneib  12362  iscnp4  12424  cnco  12427  cncnp  12436  cnrest2  12442  lmss  12452  txcnp  12477  txcn  12481  cnmpt12  12493  cnmpt22  12500  hmeof1o  12515  psmetres2  12539  distspace  12541  ismeti  12552  isxmetd  12553  xmetpsmet  12575  xblss2ps  12610  xblss2  12611  blcntrps  12621  blcntr  12622  blin2  12638  mopni3  12690  metequiv2  12702  bdmet  12708  xmettx  12716  cnbl0  12740  cnblcld  12741  tgioo  12752  elcncf1di  12772  dedekindeulemlu  12805  suplociccex  12809  dedekindicclemlu  12814  dedekindicc  12817  ivthinclemlopn  12820  ivthdec  12828  cnplimcim  12842  limccnp2lem  12851  dvfvalap  12856  reeff1olem  12898  sin0pilem1  12908  pilem3  12910  ptolemy  12951  sincosq1sgn  12953  sinq12gt0  12957  ioocosf1o  12981  rprelogbmulexp  13079  bj-nnan  13117  bdop  13242  bdunexb  13287  bj-om  13304  findset  13312  bj-peano4  13322  bj-inf2vn  13341  bj-inf2vn2  13342  pwle2  13364  pwf1oexmid  13365  nninfalllemn  13375  sbthom  13394  qdencn  13395  trilpolemlt1  13407
  Copyright terms: Public domain W3C validator