ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3jca Unicode version

Theorem 3jca 1123
Description: Join consequents with conjunction. (Contributed by NM, 9-Apr-1994.)
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
StepHypRef Expression
1 3jca.1 . . 3  |-  ( ph  ->  ps )
2 3jca.2 . . 3  |-  ( ph  ->  ch )
3 3jca.3 . . 3  |-  ( ph  ->  th )
41, 2, 3jca31 302 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  /\  th )
)
5 df-3an 926 . 2  |-  ( ( ps  /\  ch  /\  th )  <->  ( ( ps 
/\  ch )  /\  th ) )
64, 5sylibr 132 1  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    /\ w3a 924
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 926
This theorem is referenced by:  3jcad  1124  mpbir3and  1126  syl3anbrc  1127  3anim123i  1128  syl3anc  1174  syl13anc  1176  syl31anc  1177  syl113anc  1186  syl131anc  1187  syl311anc  1188  syl33anc  1189  syl133anc  1197  syl313anc  1198  syl331anc  1199  syl333anc  1206  3jaob  1238  mp3and  1276  issod  4137  tfrlemibxssdm  6074  tfr1onlembxssdm  6090  tfrcllembxssdm  6103  ltexnqq  6946  enq0tr  6972  prarloc  7041  addclpr  7075  nqprxx  7084  mulclpr  7110  ltexprlempr  7146  recexprlempr  7170  cauappcvgprlemcl  7191  caucvgprlemcl  7214  caucvgprprlemcl  7242  le2tri3i  7572  ltmul1  8045  nn0ge2m1nn  8703  nn0ge0div  8803  eluzp1p1  9013  peano2uz  9040  ledivge1le  9172  elioc2  9323  elico2  9324  elicc2  9325  iccsupr  9353  uzsubsubfz  9430  fzrev3  9468  elfz1b  9471  fseq1p1m1  9475  elfz0ubfz0  9501  elfz0fzfz0  9502  fz0fzelfz0  9503  fz0fzdiffz0  9506  elfzmlbp  9508  elfzo2  9526  elfzo0  9558  fzo1fzo0n0  9559  elfzo0z  9560  fzofzim  9564  elfzo1  9566  ubmelfzo  9576  elfzodifsumelfzo  9577  elfzom1elp1fzo  9578  fzossfzop1  9588  ssfzo12bi  9601  subfzo0  9618  fldiv4p1lem1div2  9677  intqfrac2  9691  intfracq  9692  modfzo0difsn  9767  iseqf1olemqcl  9880  iseqf1olemnab  9882  iseqf1olemab  9883  seq3f1olemqsumkj  9892  seq3f1olemqsumk  9893  seq3f1olemstep  9895  remullem  10270  qdenre  10600  maxabslemval  10606  isummolem2a  10735  fisum  10742  fsum3  10743  fisumcvg3  10752  fsumcl2lem  10755  fsumadd  10763  sumsplitdc  10789  fsummulc2  10805  divconjdvds  10932  addmodlteqALT  10942  ltoddhalfle  10975  4dvdseven  10999  dfgcd2  11085  rppwr  11099  qredeq  11160  divgcdcoprmex  11166  cncongr1  11167  dvdsnprmd  11189  oddprmge3  11198
  Copyright terms: Public domain W3C validator