Theorem 3jca 819

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 777	. 2 |- ((ps /\ ch /\ th) <-> ((ps /\ ch) /\ th))
7	5, 6	sylibr 200	1 |- (ph -> (ps /\ ch /\ th))

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

This theorem is referenced by:  3jcad 820  syl3anc 858  tpss 2476  ordelord 2970  limuni3 3123  tz7.49 3959  alephval3 4903  ltexpq 5080  le2tri3 5589  divdivdivt 5785  divdiv23t 5792  divdivmult 5795  ltmul12it 5841  ltdivmultOLD 5868  ledivmultOLD 5869  lt2mul2divt 5872  lediv2t 5891  ltdiv23t 5892  lediv23t 5893  ledivp1t 5905  flval3t 6239  flhalft 6246  quoremz 6251  quoremOLD 6252  intfrac 6253  elioo4g 6385  iccsupr 6398  lbicc2t 6404  ubicc2t 6405  uztrn 6428  eluzp1p1t 6435  peano2uz 6447  eluzfz1t 6487  elfzuzt 6488  eluzfz2t 6489  elfz2nn0t 6495  fznn0sub2t 6499  elfzp1 6510  fzrev3t 6514  fseqsupub 6526  expsubt 6598  expordit 6600  expubndt 6608  bernneq 6652  expnbndt 6654  absdivz 6859  seq1ublem 6911  facdivt 6942  facndivt 6943  faclbnd 6945  faclbnd3 6947  bcnp11t 6965  permnnt 6973  fsumcmp0 7041  serzcmp0 7055  climaddc1 7118  climmullem4 7123  climsub 7130  climsubc2 7131  climcmpc1 7139  iserzcmp 7142  caucvg3a 7164  caucvg3lem 7166  iserzabslem 7178  expcnv 7233  georeclim 7240  geoisum1c 7245  cvgratlem2 7251  efaddlem5 7342  efaddlem10 7347  efaddlem16 7353  efaddlem19 7356  efaddlem23 7360  efaddlem26 7363  ef1tllem 7381  ef01tllem1 7383  ef01tllem2 7384  ef01tllem2OLD 7385  eirrlem2 7390  eflegeolem1 7413  eflegeolem2 7414  efcnlem1 7419  reeff1o 7426  sin02gt0 7478  acdc3lem 7486  acdc2lem2 7489  acdc5lem2 7492  infxp 7572  clsndisj 7706  cnco 7768  cnpco 7769  blss 7853  ssblex 7856  methausi 7881  metcnpf 7883  metcnplem 7886  tgioolem 7914  lmuni 7951  lmle 7960  bopcnlem2 7982  iscms2lem4 7992  cmsss 7997  bcthlem8 8006  bcthlem9 8007  bcthlem18 8016  grpidinvlem2 8049  grpidinvlem4 8051  grpinvid1 8072  grpinvid2 8073  grplcan 8075  grp2inv 8078  grpinvf 8079  grpinvop 8080  grpmuldivass 8088  grppncan 8090  grpnpcan 8091  grppnpcan2 8092  grpnpncan 8094  abl4 8105  abldivdiv4 8109  ablnnncan 8111  ablnnncan1 8113  cnring 8162  ringsn 8163  vc0 8188  vcm 8190  vcoprne 8198  isnvi 8232  nvmdi 8270  nvmul0or 8272  nvsubadd 8275  nvpncan2 8276  nvnpcan 8280  nvnncan 8283  nvmeq0 8284  nvdif 8293  nvabs 8301  nvelbl 8325  nvcnpf 8328  nvlmle 8333  sqcn 8335  nmcn3 8341  nmcnc 8342  sm1cnilem 8347  sspg 8387  ssps 8389  lno0 8417  lnomul 8421  nvcnpi3 8422  nvcnpi4 8423  nmoub3i 8436  nmblore 8446  nmblolbii 8459  blocni 8465  ipasslem4 8493  ubthlem12 8540  minveclem30 8574  htthlem10 8629  psasym 8651  pstr 8652  pilem1 8671  efif1lem1 8730  efif1lem2 8731  osumlem3 9580  elunop2t 9938  nmbdoplb 9949  nmcopexlem3 9953  nmcopexlem5 9955  nmcoplb 9958  nmophm 9961  lnopcon 9963  nmbdfnlb 9978  nmcfnexlem3 9982  nmcfnexlem5 9984  nmcfnlb 9987  lnfncon 9990  riesz3 9995  cnlnadjlem2 10001  cnlnadjlem7 10006  nmopadjlem 10022  nmopco 10028  leopnmidt 10071  nmopleidt 10072  hmopidmchlem 10078  pjclem4 10127  pj3s 10135  stle 10167  hstrlem3a 10187  csmdsym 10261  superpos 10281  atexcht 10308  atcvatlem 10312  atcvat4 10324  cdj3 10368  cdrci 10494  truni1 10499  cmphmp 10521  idhme 10522  cnvhmpha 10525  cnvhmphb 10526  hmphre 10530  hmpher 10536  hmeogrp 10538  eqindhome 10541  hmeobc 10542  oefil2 10567  neifil 10568  filintf 10569  fgsb 10570  fgsbOLD 10571  fgsb2 10580  rcfpfil 10597  rcfpfilOLD 10598  dtt2 10618  mslb1 10629  iintlem1 10632  iint 10634  trnij 10637  homgrf 10730  imonclem 10741  ismonc 10742  idmon 10745  immon 10746  idfisf 10760

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 777

Copyright terms: Public domain