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

Theorem 3jca 1144
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 305 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  /\  th )
)
5 df-3an 947 . 2  |-  ( ( ps  /\  ch  /\  th )  <->  ( ( ps 
/\  ch )  /\  th ) )
64, 5sylibr 133 1  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 947
This theorem is referenced by:  3jcad  1145  mpbir3and  1147  syl3anbrc  1148  3anim123i  1149  syl3anc  1199  syl13anc  1201  syl31anc  1202  syl113anc  1211  syl131anc  1212  syl311anc  1213  syl33anc  1214  syl133anc  1222  syl313anc  1223  syl331anc  1224  syl333anc  1231  3jaob  1263  mp3and  1301  issod  4209  tfrlemibxssdm  6190  tfr1onlembxssdm  6206  tfrcllembxssdm  6219  ctssdccl  6962  ltexnqq  7180  enq0tr  7206  prarloc  7275  addclpr  7309  nqprxx  7318  mulclpr  7344  ltexprlempr  7380  recexprlempr  7404  cauappcvgprlemcl  7425  caucvgprlemcl  7448  caucvgprprlemcl  7476  suplocexprlemex  7494  le2tri3i  7836  ltmul1  8317  nn0ge2m1nn  8991  nn0ge0div  9092  eluzp1p1  9303  peano2uz  9330  ledivge1le  9464  elioc2  9670  elico2  9671  elicc2  9672  iccsupr  9700  uzsubsubfz  9778  fzrev3  9818  elfz1b  9821  fseq1p1m1  9825  elfz0ubfz0  9853  elfz0fzfz0  9854  fz0fzelfz0  9855  fz0fzdiffz0  9858  elfzmlbp  9860  elfzo2  9878  elfzo0  9910  fzo1fzo0n0  9911  elfzo0z  9912  fzofzim  9916  elfzo1  9918  ubmelfzo  9928  elfzodifsumelfzo  9929  elfzom1elp1fzo  9930  fzossfzop1  9940  ssfzo12bi  9953  subfzo0  9970  fldiv4p1lem1div2  10029  intqfrac2  10043  intfracq  10044  modfzo0difsn  10119  iseqf1olemqcl  10210  iseqf1olemnab  10212  iseqf1olemab  10213  seq3f1olemqsumkj  10222  seq3f1olemqsumk  10223  seq3f1olemstep  10225  remullem  10594  qdenre  10925  maxabslemval  10931  xrmaxiflemval  10970  summodclem2a  11101  fsum3  11107  fsum3cvg3  11116  fsumcl2lem  11118  fsumadd  11126  sumsplitdc  11152  fsummulc2  11168  isumlessdc  11216  sin02gt0  11380  divconjdvds  11454  addmodlteqALT  11464  ltoddhalfle  11497  4dvdseven  11521  dfgcd2  11609  rppwr  11623  qredeq  11684  divgcdcoprmex  11690  cncongr1  11691  dvdsnprmd  11713  oddprmge3  11722  ennnfoneleminc  11830  ctinf  11849  upxp  12347  bdmopn  12579  suplociccex  12678
  Copyright terms: Public domain W3C validator