Theorem 3jca 1050

Description: Join consequents with conjunction.

Hypotheses

Ref	Expression
3jca.1	|- (ph -> ps)
3jca.2	|- (ph -> ch)
3jca.3	|- (ph -> th)

Assertion

Ref	Expression
3jca	|- (ph -> (ps /\ ch /\ th))

Proof of Theorem 3jca

Step	Hyp	Ref	Expression
1		3jca.1	. . 3 |- (ph -> ps)
2		3jca.2	. . 3 |- (ph -> ch)
3		3jca.3	. . 3 |- (ph -> th)
4	1, 2, 3	jca31 311	. 2 |- (ph -> ((ps /\ ch) /\ th))
5		df-3an 860	. 2 |- ((ps /\ ch /\ th) <-> ((ps /\ ch) /\ th))
6	4, 5	sylibr 217	1 |- (ph -> (ps /\ ch /\ th))

Syntax hints:   -> wi 3   /\ wa 240   /\ w3a 858

This theorem is referenced by:  3jcad 1051  syl3ancOLD 1096  syl3an2cOLD 1097  syl111anc 1100  syl13anc 1102  syl31anc 1103  syl32anc 1108  syl113anc 1112  syl131anc 1113  syl311anc 1114  syl33anc 1115  syl133anc 1120  syl313anc 1121  syl331anc 1122  syl333anc 1129  3jaob 1159  tpssOLD 3146  limuni3 3936  onfununi 5116  tz7.49 5168  ordtypelem7 5690  hartog 5693  omsublim 5887  alephval3 6051  ltexpq 6232  le2tri3i 6764  ltmul12a 7023  ltdivmulOLD 7050  ledivmulOLD 7052  intfrac2 7495  intfracq 7496  elioo4g 7553  iccsupr 7567  lbicc2 7573  ubicc2 7574  uztrn 7597  eluzp1p1 7604  peano2uz 7616  elfzuz 7658  elfz2nn0 7667  fznn0sub2 7671  elfzp1 7683  fzrev3 7692  expordi 7845  seq1ublem 8163  fsumcmp0 8301  serzcmp0 8315  climaddc1 8378  climmullem4 8383  climsub 8390  climsubc2 8391  climcmpc1 8399  iserzcmp 8402  caucvg3ai 8424  caucvg3lem 8426  iserzabslem 8438  expcnv 8494  cvgratlem2ALT 8510  cvgratlem2 8513  efaddlem10 8609  efaddlem16 8615  efaddlem19 8618  efaddlem26 8625  ef1tllem 8643  ef01tllem2 8646  ef01tllem2OLD 8647  eirrlem2 8652  eflegeolem2 8679  efcnlem1 8684  sin02gt0 8744  acdc3lem 8754  acdc5lem2 8761  infxp 8841  cnpnei 9043  cnco 9045  cnpco 9046  metcnpf 9161  tgioolem 9192  lmuni 9229  lmle 9238  bopcnlem2 9260  iscms2lem4 9270  cmsss 9275  bcthlem8 9284  bcthlem9 9285  grpidinvlem2 9329  grpinvid1 9356  grpinvid2 9357  grplcan 9359  grp2inv 9363  grpinvf 9364  grpmuldivass 9373  grpnpncan 9379  abl4 9413  abldivdiv4 9417  ablnnncan 9419  ablnnncan1 9421  ga0 9453  gaid 9454  ssga 9455  gacan 9460  ringlz 9487  ringrz 9488  cnring 9489  ringsn 9490  vc0 9520  vcoprne 9530  isnvi 9564  nvmdi 9602  nvsubadd 9607  nvnpcan 9612  nvmeq0 9616  nvabs 9633  nvelbl 9657  nvcnpf 9660  vacnlem5 9671  sqcn 9674  nmcn3 9680  nmcnc 9681  sspg 9726  ssps 9728  lno0 9756  lnomul 9760  nvcnpi3 9761  nvcnpi4 9762  nmoub3i 9775  nmblore 9786  nmblolbii 9799  ubthlem12 9883  ubthlem12OLD 9884  minveclem30 9919  htthlem10 9976  psasym 9994  pstr 9995  pilem1 10020  efif1lem1 10084  efif1lem2 10085  cdrci 10182  hausnei2 10222  upxp 10225  txcn 10227  hmeobc 10239  cnvhmpha 10240  filintf 10274  oefil2 10275  filfbas 10276  fsubbas 10281  fgfil 10290  extbas1 10291  filrn 10293  limfil 10297  neifil 10302  elfilmap3 10314  fbaslim 10322  isflimf 10323  ismnd1 10391  unmnd 10405  osumlem3 11215  elunop2 11575  nmophmi 11598  cnlnadjlem7 11643  nmopcoi 11665  hmopidmchlem 11722  pjclem4 11772  pj3si 11780  stlei 11812  hstrlem3a 11832  csmdsymi 11906  atexch 11953  atcvatlem 11957  atcvat4i 11969  cdj3i 12013  bnj951 12848  bnj1064 12900  bnj1363 13090  bnj578 13291  bnj605 13292  bnj607 13304  bnj908 13329  bnj1001 13366  bnj1110 13417  bnj1128 13428  bnj1173 13441  zmodfz 13615  gcdcllem3 13720  poseq 13954  wfrlem15 13971  elno2 14005  axfelem17 14047  surjsec 14462  injsurinj 14487  cbcpcp 14504  cbicplem 14508  unprj 14511  cljo 14534  clme 14535  int2pre 14578  sqpre 14579  inposet 14620  definc 14621  dfps2 14634  toplat 14638  dfdir2 14639  reacomsmgrp1 14703  reacomsmgrp3 14705  reacomsmgrp4 14706  resgcom 14712  fprodadd 14713  seqzp2 14716  ltlga 14729  gaplc 14731  curgrpact 14735  grpdrcan 14738  grpdlcan 14739  trooo 14758  zerdivemp1 14785  dblsubvec 14817  mvecrtol2 14820  svli2 14826  vri 14834  truni1 14849  truni3 14851  cbci 14852  cmphmp 14878  idhme 14879  cnvhmphb 14880  hmphre 14884  hmpher 14890  hmeogrp 14892  eqindhome 14895  istopx 14918  fgsb 14921  fgsb2 14925  rcfpfil 14934  limvinlv 14941  limfilnei 14943  cnpfillim4 14947  dtt2 14951  topgrpsubcnlem 14981  trhom 14983  altretop 14997  cntrsetlem 14999  mslb1 15007  iintlem1 15010  iint 15012  trnij 15015  flimfnein 15033  lvsovso 15038  lvsovso2 15039  lvsovso3 15040  supnuf 15041  dualalg 15131  dualded 15132  dualcat2 15133  homgrf 15151  imonclem 15162  ismonc 15163  idmon 15166  immon 15167  iepiclem 15172  isepic 15173  idfisf 15189  idsubfun 15206  cptarc 15242  tartarmap 15265  cartarlim 15282  fnctartar 15284  fnctartar2 15285  isline1 15294  elfiun 15369  inficlALT 15372  ordtypelem7OLD 15381  hartogOLD 15384  omsublimOLD 15396  hmeoclda 15421  hmeocldb 15422  connsub 15443  reconnlem1 15446  reconnlem3 15448  reconnlem4 15449  2ndcctbss 15478  finlocfin 15509  locfindsc 15515  locfincf 15516  opnfbas 15557  supfil 15560  isufil2 15565  ufprim 15569  filssufillem 15570  ufinffr 15578  ufilen 15579  filcon 15580  limfilcf 15587  flimcls 15588  cnpfillim 15589  rnelfmlem 15592  rnelfm 15593  fmfnfmlem2 15595  fmfnfmlem4 15597  fmfnfm 15598  filclus 15605  flimfnfcls 15615  ufcomp 15622  tailfb 15639  filnetlem1 15640  filnetlem3 15642  filnetlem4 15643  filnetlem5 15644  upixp 15729  fimax 15746  indexa 15753  fzn0 15789  fzsplit 15792  elnnr 15803  fdc 15812  seqpo 15814  nnubfi 15818  nninfnub 15819  fsumlt1 15831  mettrifi 15847  geomcau 15849  iccsplit 15854  iirev 15871  iihalf1 15872  iihalf2 15873  iimulcl 15874  icoopnst 15876  iocopnst 15877  hmeocnv 15898  tlmconst 15907  sstotbnd 15936  heiborlem13 15967  heiborlem16 15970  heiborlem32 15986  rrndstprj2 16018  isgrpda 16033  phtpycom 16050  reparpht 16065  pcohtpylem3 16082  pcopt 16084  pcoass 16085  pcorevlem 16086  pcorev 16087  pi1bval 16088  pi1gp 16095  isringd 16097  zerdivemp1x 16108  rnghomsub 16127  rnghomco 16128  rngisocnv 16135  crngm4 16151  rngidl 16172  0idl 16173  intidl 16177  unichnidl 16179  keridl 16180  smprngpr 16200  igenval 16209  igenval2 16214  prnc 16215  isfldidl 16216  pm13.194 16376  smoiso 16453  posref 16775  isposiNEW 16778  posgelem 16795  posgeref 16796  latjlej1 16866  latmlem1 16876  latledi 16884  latjass 16886  latj23 16887  lubss 16897  isopi 16910  latm12 16955  omllaw5 16968  cmtcomlem 16969  cmtbr3 16975  omlfh3 16979  cvr1 17054  cvrexchlem 17059  cvratlem 17061  cvrntr 17063  atcvrj2b 17069  atltcvr 17072  atexchcvr 17073  cvrat4 17076  ps-1 17078  grpidinvlem2NEW 17110  grpinvid1NEW 17131  grpinvid2NEW 17132  grplcanNEW 17134  ringlzNEW 17156  ringrzNEW 17157  paddval 17259  padd01 17272  padd02 17273  paddss12 17280  paddasslem2 17282  paddasslem4 17284  paddasslem6 17286  paddasslem9 17289  paddasslem10 17290  paddasslem12 17292  paddasslem15 17295  pmodlem1 17307  pmod2i 17310  pmod 17311  pmapjat 17314  paddun 17337  poml4 17361  poml5 17362  osumcllem6 17369  osumcl 17375  pexmidlem6 17383  pl42lem2 17408  pl42lem3 17409

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 164  df-an 242  df-3an 860

Copyright terms: Public domain