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

Theorem 3jca 1095
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 296 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  /\  th )
)
5 df-3an 898 . 2  |-  ( ( ps  /\  ch  /\  th )  <->  ( ( ps 
/\  ch )  /\  th ) )
64, 5sylibr 141 1  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    /\ w3a 896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  3jcad  1096  mpbir3and  1098  syl3anbrc  1099  3anim123i  1100  syl3anc  1146  syl13anc  1148  syl31anc  1149  syl113anc  1158  syl131anc  1159  syl311anc  1160  syl33anc  1161  syl133anc  1169  syl313anc  1170  syl331anc  1171  syl333anc  1178  3jaob  1208  mp3and  1246  issod  4083  tfrlemibxssdm  5971  ltexnqq  6563  enq0tr  6589  prarloc  6658  addclpr  6692  nqprxx  6701  mulclpr  6727  ltexprlempr  6763  recexprlempr  6787  cauappcvgprlemcl  6808  caucvgprlemcl  6831  caucvgprprlemcl  6859  le2tri3i  7184  ltmul1  7656  nn0ge2m1nn  8298  nn0ge0div  8384  eluzp1p1  8593  peano2uz  8621  ledivge1le  8749  elioc2  8905  elico2  8906  elicc2  8907  iccsupr  8935  uzsubsubfz  9012  fzrev3  9050  elfz1b  9053  fseq1p1m1  9057  elfz0ubfz0  9083  elfz0fzfz0  9084  fz0fzelfz0  9085  fz0fzdiffz0  9088  elfzmlbmOLD  9090  elfzmlbp  9091  elfzo2  9108  elfzo0  9139  fzo1fzo0n0  9140  elfzo0z  9141  fzofzim  9145  elfzo1  9147  ubmelfzo  9157  elfzodifsumelfzo  9158  elfzom1elp1fzo  9159  fzossfzop1  9169  ssfzo12bi  9182  subfzo0  9198  fldiv4p1lem1div2  9249  intqfrac2  9263  intfracq  9264  modfzo0difsn  9339  remullem  9692  qdenre  10021  divconjdvds  10153  addmodlteqALT  10163  ltoddhalfle  10197  4dvdseven  10221
  Copyright terms: Public domain W3C validator