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  6355  elni2  6410  dfplpq2  6450  dfmpq2  6451  enqbreq2  6453  enqdc1  6458  addcmpblnq  6463  addclnq  6471  nqpi  6474  addassnqg  6478  mulassnqg  6480  mulcanenq  6481  distrnqg  6483  1qec  6484  recexnq  6486  subhalfnqq  6510  enq0tr  6530  nqnq0pi  6534  nq0nn  6538  mulcanenq0ec  6541  nnnq0lem1  6542  addclnq0  6547  distrnq0  6555  addassnq0lemcl  6557  elnp1st2nd  6572  prarloc  6599  addlocprlemlt  6627  addlocprlemeq  6629  addlocprlemgt  6630  addclpr  6633  nqprm  6638  mullocprlem  6666  mullocpr  6667  mulclpr  6668  ltpopr  6691  ltaddpr  6693  ltexprlemm  6696  ltexprlemopl  6697  ltexprlemopu  6699  ltexprlemrnd  6701  ltexprlemdisj  6702  addcanprleml  6710  addcanprlemu  6711  addcanprg  6712  recexprlemm  6720  recexprlemopl  6721  recexprlemopu  6723  recexprlemrnd  6725  recexprlemdisj  6726  cauappcvgprlemm  6741  cauappcvgprlemopl  6742  cauappcvgprlemopu  6744  cauappcvgprlemrnd  6746  cauappcvgprlemdisj  6747  cauappcvgprlemlim  6757  caucvgprlemnkj  6762  caucvgprlemm  6764  caucvgprlemopl  6765  caucvgprlemopu  6767  caucvgprlemrnd  6769  caucvgprlemlim  6777  caucvgprprlemnkltj  6785  caucvgprprlemnkeqj  6786  caucvgprprlemnjltk  6787  caucvgprprlemm  6792  caucvgprprlemopl  6793  caucvgprprlemopu  6795  caucvgprprlemrnd  6797  caucvgprprlemexbt  6802  caucvgprprlemlim  6807  prsrlem1  6825  mulclsr  6837  mulasssrg  6841  distrsrg  6842  elreal2  6905  axmulass  6945  axdistr  6946  axcaucvglemcau  6970  add20  7467  mullt0  7473  rereim  7575  ltmul1  7581  cru  7591  mulap0r  7604  divmuldivap  7686  divmuleqap  7691  divadddivap  7701  divmuldivapd  7804  ltmul12a  7824  lemul12a  7826  lemulge11  7830  lediv12a  7858  lediv2a  7859  recgt1i  7862  recreclt  7864  ledivp1  7867  lemul1ad  7903  lemul2ad  7904  ltmul12ad  7905  lemul12ad  7906  lemul12bd  7907  nndivre  7947  nndivtr  7953  halfaddsubcl  8156  halfaddsub  8157  lt2halves  8158  nnrecl  8177  elnn0nn  8222  elnnnn0b  8224  elnnnn0c  8225  nn0addge1  8226  nn0addge2  8227  elnn0z  8256  elnnz1  8266  elz2  8310  zdivadd  8327  zdivmul  8328  zextle  8329  peano2uz2  8343  uzind  8347  btwnz  8355  uzss  8491  eluzp1m1  8494  eluz2b2  8538  qre  8558  qaddcl  8568  qmulcl  8570  qreccl  8574  irradd  8578  irrmul  8579  cnref1o  8580  rprege0  8595  rprene0  8598  rpreap0  8599  rpcnne0  8600  rpcnap0  8601  rpregt0d  8627  rprege0d  8628  rprene0d  8629  rpcnne0d  8630  lediv2ad  8643  ledivge1le  8650  lediv12ad  8680  xrlttri3  8716  xrrebnd  8730  xrrege0  8736  elioo4g  8801  ioomax  8815  iccmax  8816  divelunit  8868  elfz5  8880  uzsubsubfz  8909  fzopth  8922  fzass4  8923  fzrev2  8945  uzsplit  8952  elfz2nn0  8971  difelfzle  8990  1fv  8994  4fvwrd4  8995  fzo1fzo0n0  9037  elfzom1elp1fzo  9056  subfzo0  9095  qtri3or  9096  adddivflid  9132  flltdivnn0lt  9144  expclzaplem  9253  leexp1a  9283  expubnd  9285  le2sq2  9303  sumsqeq0  9306  bernneq  9343  expnlbnd  9347  shftlem  9391  shftfvalg  9393  shftfval  9396  cvg1nlemcau  9557  cvg1nlemres  9558  rexuz3  9562  resqrexlemcvg  9591  resqrexlemglsq  9594  resqrexlemga  9595  sqrtle  9608  sqrtlt  9609  sqrt11  9611  sqrtsq2  9615  absmul  9641  sqabs  9652  abslt  9658  absle  9659  lenegsq  9665  climcn2  9804  mulcn2  9807  sqr2irrlem  9851  bdop  9969  bdunexb  10014  bj-om  10035  findset  10044  bj-peano4  10054  bj-inf2vn  10073  bj-inf2vn2  10074  qdencn  10097
  Copyright terms: Public domain W3C validator