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

Theorem jca 290
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 126 . 2  |-  ( ps 
->  ( ch  ->  ( ps  /\  ch ) ) )
41, 2, 3sylc 56 1  |-  ( ph  ->  ( ps  /\  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101
This theorem is referenced by:  jca31  292  jca32  293  jcai  294  jctil  295  jctir  296  ancli  306  ancri  307  sylanbrc  394  jcab  535  ioran  669  ordi  729  dfandc  778  stabtestimpdc  824  pm4.55dc  846  mpbi2and  850  mpbir2and  851  pm4.82  857  pm4.83dc  858  rnlem  883  syl22anc  1136  syl112anc  1139  syl121anc  1140  syl211anc  1141  syl23anc  1142  syl32anc  1143  syl122anc  1144  syl212anc  1145  syl221anc  1146  syl222anc  1151  syl123anc  1152  syl132anc  1153  syl213anc  1154  syl231anc  1155  syl312anc  1156  syl321anc  1157  syl223anc  1161  syl232anc  1162  syl322anc  1163  syl233anc  1164  syl323anc  1165  syl332anc  1166  ecased  1239  19.26  1370  nfand  1460  19.40  1522  equsexd  1617  sbcof2  1691  sbequ8  1727  eu2  1944  eu3h  1945  eu5  1947  mooran2  1973  datisi  2010  felapton  2014  darapti  2015  dimatis  2017  fresison  2018  fesapo  2020  r19.26  2441  r19.29af2  2452  r19.40  2464  eqvinc  2667  eqvincg  2668  reu6  2730  reu3  2731  indifdir  3193  undif3ss  3198  un00  3263  disjpr2  3434  prel12  3542  prneimg  3545  preqsn  3546  opexgOLD  3965  opth  3974  0nelop  3985  euotd  3991  opelopabsb  3997  ispod  4041  elon2  4113  unexb  4177  opeluu  4182  eusvnfb  4186  suc11g  4281  nlimsucg  4290  tfi  4305  vtoclr  4388  opthprc  4391  ideqg  4487  resiexg  4653  dminss  4738  imainss  4739  ssxpbm  4756  relrelss  4844  funopg  4934  fntpg  4955  fun11uni  4969  imain  4981  funimaexglem  4982  funssxp  5060  ffdm  5061  f00  5081  dffo2  5110  fodmrnu  5114  foco  5116  fun11iun  5147  f1o00  5161  fv3  5197  dff2  5311  dff3im  5312  dffo4  5315  ffnfv  5323  ffvresb  5328  fsn2  5337  fconstfvm  5379  fnfvima  5393  fcof1o  5429  isocnv  5451  isotr  5456  riotaprop  5491  acexmidlemcase  5507  caovlem2d  5693  f1ocnvd  5702  caofcom  5734  resfunexgALT  5737  elxp7  5797  2ndrn  5809  1stconst  5842  2ndconst  5843  cnvf1olem  5845  poxp  5853  dftpos4  5878  dfsmo2  5902  tfrlem5  5930  tfrlemiex  5945  rdgon  5973  frecabex  5984  frecrdg  5992  oawordi  6049  nntri3  6075  nnmordi  6089  iserd  6132  relelec  6146  erth  6150  qliftfun  6188  bren  6228  findcard2d  6348  findcard2sd  6349  nnwetri  6354  ordiso2  6357  elni2  6412  dfplpq2  6452  dfmpq2  6453  enqbreq2  6455  enqdc1  6460  addcmpblnq  6465  addclnq  6473  nqpi  6476  addassnqg  6480  mulassnqg  6482  mulcanenq  6483  distrnqg  6485  1qec  6486  recexnq  6488  subhalfnqq  6512  enq0tr  6532  nqnq0pi  6536  nq0nn  6540  mulcanenq0ec  6543  nnnq0lem1  6544  addclnq0  6549  distrnq0  6557  addassnq0lemcl  6559  elnp1st2nd  6574  prarloc  6601  addlocprlemlt  6629  addlocprlemeq  6631  addlocprlemgt  6632  addclpr  6635  nqprm  6640  mullocprlem  6668  mullocpr  6669  mulclpr  6670  ltpopr  6693  ltaddpr  6695  ltexprlemm  6698  ltexprlemopl  6699  ltexprlemopu  6701  ltexprlemrnd  6703  ltexprlemdisj  6704  addcanprleml  6712  addcanprlemu  6713  addcanprg  6714  recexprlemm  6722  recexprlemopl  6723  recexprlemopu  6725  recexprlemrnd  6727  recexprlemdisj  6728  cauappcvgprlemm  6743  cauappcvgprlemopl  6744  cauappcvgprlemopu  6746  cauappcvgprlemrnd  6748  cauappcvgprlemdisj  6749  cauappcvgprlemlim  6759  caucvgprlemnkj  6764  caucvgprlemm  6766  caucvgprlemopl  6767  caucvgprlemopu  6769  caucvgprlemrnd  6771  caucvgprlemlim  6779  caucvgprprlemnkltj  6787  caucvgprprlemnkeqj  6788  caucvgprprlemnjltk  6789  caucvgprprlemm  6794  caucvgprprlemopl  6795  caucvgprprlemopu  6797  caucvgprprlemrnd  6799  caucvgprprlemexbt  6804  caucvgprprlemlim  6809  prsrlem1  6827  mulclsr  6839  mulasssrg  6843  distrsrg  6844  elreal2  6907  axmulass  6947  axdistr  6948  axcaucvglemcau  6972  add20  7469  mullt0  7475  rereim  7577  ltmul1  7583  cru  7593  mulap0r  7606  divmuldivap  7688  divmuleqap  7693  divadddivap  7703  divmuldivapd  7806  ltmul12a  7826  lemul12a  7828  lemulge11  7832  lediv12a  7860  lediv2a  7861  recgt1i  7864  recreclt  7866  ledivp1  7869  lemul1ad  7905  lemul2ad  7906  ltmul12ad  7907  lemul12ad  7908  lemul12bd  7909  nndivre  7949  nndivtr  7955  halfaddsubcl  8158  halfaddsub  8159  lt2halves  8160  nnrecl  8179  elnn0nn  8224  elnnnn0b  8226  elnnnn0c  8227  nn0addge1  8228  nn0addge2  8229  elnn0z  8258  elnnz1  8268  elz2  8312  zdivadd  8329  zdivmul  8330  zextle  8331  peano2uz2  8345  uzind  8349  btwnz  8357  uzss  8493  eluzp1m1  8496  eluz2b2  8540  qre  8560  qaddcl  8570  qmulcl  8572  qreccl  8576  irradd  8580  irrmul  8581  cnref1o  8582  rprege0  8597  rprene0  8600  rpreap0  8601  rpcnne0  8602  rpcnap0  8603  rpregt0d  8629  rprege0d  8630  rprene0d  8631  rpcnne0d  8632  lediv2ad  8645  ledivge1le  8652  lediv12ad  8682  xrlttri3  8718  xrrebnd  8732  xrrege0  8738  elioo4g  8803  ioomax  8817  iccmax  8818  divelunit  8870  elfz5  8882  uzsubsubfz  8911  fzopth  8924  fzass4  8925  fzrev2  8947  uzsplit  8954  elfz2nn0  8973  difelfzle  8992  1fv  8996  4fvwrd4  8997  fzo1fzo0n0  9039  elfzom1elp1fzo  9058  subfzo0  9097  qtri3or  9098  adddivflid  9134  flltdivnn0lt  9146  intfracq  9162  expclzaplem  9279  leexp1a  9309  expubnd  9311  le2sq2  9329  sumsqeq0  9332  bernneq  9369  expnlbnd  9373  shftlem  9417  shftfvalg  9419  shftfval  9422  cvg1nlemcau  9583  cvg1nlemres  9584  rexuz3  9588  resqrexlemcvg  9617  resqrexlemglsq  9620  resqrexlemga  9621  sqrtle  9634  sqrtlt  9635  sqrt11  9637  sqrtsq2  9641  absmul  9667  sqabs  9678  abslt  9684  absle  9685  lenegsq  9691  climcn2  9830  mulcn2  9833  sqr2irrlem  9877  bdop  9995  bdunexb  10040  bj-om  10061  findset  10070  bj-peano4  10080  bj-inf2vn  10099  bj-inf2vn2  10100  qdencn  10124
  Copyright terms: Public domain W3C validator