Theorem 3jca 831

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

Syntax hints:   -> wi 3   /\ wa 230   /\ w3a 787

This theorem is referenced by:  3jcad 832  syl3anc 870  tpss 2530  ordelord 3027  limuni3 3180  tz7.49 4017  alephval3 4968  ltexpq 5145  le2tri3i 5654  divdivdiv 5843  divdiv23 5850  divdivmul 5853  ltmul12a 5899  ltdivmulOLD 5926  ledivmulOLD 5928  lt2mul2div 5931  lediv2 5951  ltdiv23 5952  lediv23 5953  ledivp1 5965  flval3 6351  flhalf 6358  quoremz 6363  quoremnn0 6365  intfrac 6366  intfracq 6367  elioo4g 6410  iccsupr 6424  lbicc2 6430  ubicc2 6431  uztrn 6454  eluzp1p1 6461  peano2uz 6473  eluzfz1 6513  elfzuz 6514  eluzfz2 6515  elfz2nn0 6521  fznn0sub2 6525  elfzp1 6536  fzrev3 6540  fseqsupubi 6552  expsub 6687  expordi 6689  expubnd 6697  bernneq 6741  expnbnd 6743  expnlbnd2 6745  absdivzi 6949  seq1ublem 7001  facdiv 7032  facndiv 7033  faclbnd 7035  faclbnd3 7037  bcnp11 7055  permnn 7063  fsumcmp0 7131  serzcmp0 7145  climaddc1 7208  climmullem4 7213  climsub 7220  climsubc2 7221  climcmpc1 7229  iserzcmp 7232  caucvg3ai 7254  caucvg3lem 7256  iserzabslem 7268  expcnv 7323  georeclim 7330  geoisum1c 7335  cvgratlem2 7341  efaddlem5 7432  efaddlem10 7437  efaddlem16 7443  efaddlem19 7446  efaddlem23 7450  efaddlem26 7453  ef1tllem 7471  ef01tllem1 7473  ef01tllem2 7474  ef01tllem2OLD 7475  eirrlem2 7480  eflegeolem1 7504  eflegeolem2 7505  efcnlem1 7510  reeff1o 7517  sin02gt0 7570  acdc3lem 7578  acdc2lem2 7581  acdc5lem2 7584  infxp 7664  clsndisj 7791  cnco 7853  cnpco 7854  blss 7938  ssblex 7941  methausi 7966  metcnpf 7968  metcnplem 7971  tgioolem 7999  lmuni 8036  lmle 8045  bopcnlem2 8067  iscms2lem4 8077  cmsss 8082  bcthlem8 8091  bcthlem9 8092  bcthlem18 8101  grpidinvlem2 8134  grpidinvlem4 8136  grpinvid1 8156  grpinvid2 8157  grplcan 8159  grp2inv 8162  grpinvf 8163  grpinvop 8164  grpmuldivass 8172  grppncan 8174  grpnpcan 8175  grppnpcan2 8176  grpnpncan 8178  abl4 8189  abldivdiv4 8193  ablnnncan 8195  ablnnncan1 8197  cnring 8246  ringsn 8247  vc0 8272  vcm 8274  vcoprne 8282  isnvi 8316  nvmdi 8354  nvmul0or 8356  nvsubadd 8359  nvpncan2 8360  nvnpcan 8364  nvnncan 8367  nvmeq0 8368  nvdif 8377  nvabs 8385  nvelbl 8409  nvcnpf 8412  nvlmle 8417  sqcn 8419  nmcn3 8425  nmcnc 8426  sm1cnilem 8431  sspg 8471  ssps 8473  lno0 8501  lnomul 8505  nvcnpi3 8506  nvcnpi4 8507  nmoub3i 8520  nmblore 8530  nmblolbii 8543  blocni 8549  ipasslem4 8577  ubthlem12 8624  minveclem30 8658  htthlem10 8713  psasym 8735  pstr 8736  pilem1 8754  efif1lem1 8813  efif1lem2 8814  osumlem3 9663  elunop2 10021  nmbdoplbi 10032  nmcopexlem3 10036  nmcopexlem5 10038  nmcoplbi 10041  nmophmi 10044  lnopconi 10046  nmbdfnlbi 10061  nmcfnexlem3 10065  nmcfnexlem5 10067  nmcfnlbi 10070  lnfnconi 10073  riesz3i 10078  cnlnadjlem2 10084  cnlnadjlem7 10089  nmopadjlem 10105  nmopcoi 10111  leopnmid 10154  nmopleid 10155  hmopidmchlem 10161  pjclem4 10211  pj3si 10219  stlei 10251  hstrlem3a 10271  csmdsymi 10345  superpos 10365  atexch 10392  atcvatlem 10396  atcvat4i 10408  cdj3i 10452  inposet 10578  vri 10583  cdrci 10588  truni1 10593  cmphmp 10615  idhme 10616  cnvhmpha 10619  cnvhmphb 10620  hmphre 10624  hmpher 10630  hmeogrp 10632  eqindhome 10635  hmeobc 10636  oefil2 10660  neifil 10661  filintf 10662  fgsb 10663  fgsb2 10668  rcfpfil 10677  dtt2 10697  mslb1 10711  iintlem1 10714  iint 10716  trnij 10719  homgrf 10812  imonclem 10823  ismonc 10824  idmon 10827  immon 10828  iepiclem 10833  isepic 10834  idfisf 10844

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 154  df-an 232  df-3an 789

Copyright terms: Public domain