Theorem 3jca 817

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	. . . 4 |- (ph -> ps)
2		3jca.2	. . . 4 |- (ph -> ch)
3	1, 2	jca 288	. . 3 |- (ph -> (ps /\ ch))
4		3jca.3	. . 3 |- (ph -> th)
5	3, 4	jca 288	. 2 |- (ph -> ((ps /\ ch) /\ th))
6		df-3an 775	. 2 |- ((ps /\ ch /\ th) <-> ((ps /\ ch) /\ th))
7	5, 6	sylibr 200	1 |- (ph -> (ps /\ ch /\ th))

Syntax hints:   -> wi 3   /\ wa 223   /\ w3a 773

This theorem is referenced by:  3jcad 818  syl3anc 856  tpss 2467  ordelord 2960  limuni3 3113  tz7.49 3944  alephval3 4875  ltexpq 5052  le2tri3 5563  divdivdivt 5741  divdiv23t 5748  divdivmult 5751  ltmul12it 5797  ltdivmult 5819  ledivmult 5820  lt2mul2divt 5822  lediv2t 5839  ltdiv23t 5840  lediv23t 5841  ledivp1t 5853  flval3t 6182  flhalft 6189  elioo4g 6318  iccsupr 6331  lbicc2t 6337  ubicc2t 6338  uztrn 6360  eluzp1p1t 6367  peano2uz 6379  eluzfz1t 6419  elfzuzt 6420  eluzfz2t 6421  elfz2nn0t 6427  fznn0sub2t 6431  elfzp1 6442  fzrev3t 6446  fseqsupub 6458  expsubt 6529  expordit 6531  expubndt 6539  bernneq 6583  expnbndt 6585  absdivz 6794  seq1ublem 6848  facdivt 6879  facndivt 6880  faclbnd 6882  faclbnd3 6884  bcnp11t 6903  permnnt 6911  fsumcmp0 6979  serzcmp0 6993  climaddc1 7054  climmullem4 7059  climsub 7066  climsubc2 7067  climcmpc1 7075  iserzcmp 7078  caucvg3a 7100  caucvg3lem 7102  iserzabslem 7114  expcnv 7168  georeclim 7175  geoisum1c 7180  cvgratlem2 7186  efaddlem5 7284  efaddlem10 7289  efaddlem16 7295  efaddlem19 7298  efaddlem23 7302  efaddlem26 7305  ef1tllem 7323  ef01tllem1 7325  ef01tllem2 7326  eirrlem2 7331  eflegeolem1 7353  eflegeolem2 7354  efcnlem1 7359  reeff1o 7368  sin02gt0 7420  acdc3lem 7428  acdc2lem2 7431  acdc5lem2 7434  infxp 7515  clsndisj 7648  cnco 7707  cnpco 7708  ssblex 7796  methausi 7820  metcnpf 7822  metcnplem 7825  tgioolem 7853  lmuni 7886  lmle 7895  bopcnlem2 7916  iscms2lem4 7926  cmsss 7931  bcthlem8 7940  bcthlem9 7941  bcthlem18 7950  grpidinvlem2 7983  grpidinvlem4 7985  grpinvid1 8006  grpinvid2 8007  grplcan 8010  grp2inv 8013  grpinvf 8014  grpinvop 8015  grpmuldivass 8023  grppncan 8025  grpnpcan 8026  grppnpcan2 8027  grpnpncan 8029  abl4 8041  abldivdiv4 8046  ablnnncan 8048  ablnnncan1 8050  cnring 8099  ringsn 8100  vc0 8125  vcm 8127  vcoprne 8136  isnvi 8171  isnviOLD 8172  nvmdi 8210  nvmul0or 8212  nvsubadd 8215  nvpncan2 8216  nvnpcan 8220  nvnncan 8223  nvmeq0 8224  nvdif 8232  nvabs 8240  nvelbl 8263  nvlmle 8268  sqcn 8270  nmcnc 8276  sm1cnilem 8281  sspg 8321  ssps 8323  lno0 8351  lnomul 8354  nvcnpi4 8355  nmoub3i 8368  nmblore 8378  nmblolbii 8390  blocni 8396  ipasslem4 8424  ubthlem12 8471  minveclem30 8505  htthlem10 8559  psasym 8576  pilem1 8590  efif1lem1 8645  efif1lem2 8646  osumlem3 9497  elunop2t 9853  nmbdoplb 9864  nmcopexlem3 9868  nmcopexlem5 9870  nmcoplb 9873  nmophm 9876  lnopcon 9878  nmbdfnlb 9893  nmcfnexlem3 9897  nmcfnexlem5 9899  nmcfnlb 9902  lnfncon 9905  riesz3 9910  cnlnadjlem2 9916  cnlnadjlem7 9921  nmopadjlem 9937  nmopco 9942  leopnmidt 9982  nmopleidt 9983  hmopidmchlem 9989  pjclem4 10037  pj3s 10045  stle 10077  hstrlem3a 10097  csmdsym 10169  superpos 10189  atexcht 10216  atcvatlem 10220  atcvat4 10232  cdj3 10273  cdrci 10381  truni1 10386  cmphmp 10408  idhme 10409  cnvhmpha 10412  cnvhmphb 10413  hmphre 10417  hmpher 10423  hmeogrp 10425  oefil2 10441  neifil 10442  filintf 10443  fgsb 10444  fgsb2 10449  dtt2 10462  mslb1 10473  msra3 10475  iintlem1 10476  iint 10478  trnij 10481  homgrf 10574  imonclem 10583  ismonc 10584  idmon 10588  immon 10589

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  df-3an 775

Copyright terms: Public domain