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

Theorem 3jca 1083
Description: Join consequents with conjunction. (Contributed by NM, 9-Apr-1994.)
Hypotheses
Ref Expression
3jca.1
3jca.2
3jca.3
Assertion
Ref Expression
3jca

Proof of Theorem 3jca
StepHypRef Expression
1 3jca.1 . . 3
2 3jca.2 . . 3
3 3jca.3 . . 3
41, 2, 3jca31 292 . 2
5 df-3an 886 . 2
64, 5sylibr 137 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   w3a 884
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110  df-3an 886
This theorem is referenced by:  3jcad  1084  mpbir3and  1086  syl3anbrc  1087  3anim123i  1088  syl3anc  1134  syl13anc  1136  syl31anc  1137  syl113anc  1146  syl131anc  1147  syl311anc  1148  syl33anc  1149  syl133anc  1157  syl313anc  1158  syl331anc  1159  syl333anc  1166  3jaob  1196  issod  4047  tfrlemibxssdm  5882  ltexnqq  6391  enq0tr  6417  prarloc  6486  addclpr  6520  nqprxx  6529  mulclpr  6553  ltexprlempr  6582  recexprlempr  6604  cauappcvgprlemcl  6625  caucvgprlemcl  6647  le2tri3i  6923  ltmul1  7376  nn0ge2m1nn  8018  nn0ge0div  8103  eluzp1p1  8274  peano2uz  8302  elioc2  8575  elico2  8576  elicc2  8577  iccsupr  8605  uzsubsubfz  8681  fzrev3  8719  elfz1b  8722  fseq1p1m1  8726  elfz0ubfz0  8752  elfz0fzfz0  8753  fz0fzelfz0  8754  fz0fzdiffz0  8757  elfzmlbmOLD  8759  elfzmlbp  8760  elfzo2  8777  elfzo0  8808  fzo1fzo0n0  8809  elfzo0z  8810  fzofzim  8814  elfzo1  8816  ubmelfzo  8826  elfzodifsumelfzo  8827  elfzom1elp1fzo  8828  fzossfzop1  8838  ssfzo12bi  8851  remullem  9099
  Copyright terms: Public domain W3C validator