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

Theorem 3jca 1119
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 922 . 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 920
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 922
This theorem is referenced by:  3jcad  1120  mpbir3and  1122  syl3anbrc  1123  3anim123i  1124  syl3anc  1170  syl13anc  1172  syl31anc  1173  syl113anc  1182  syl131anc  1183  syl311anc  1184  syl33anc  1185  syl133anc  1193  syl313anc  1194  syl331anc  1195  syl333anc  1202  3jaob  1234  mp3and  1272  issod  4102  tfrlemibxssdm  5997  tfr1onlembxssdm  6013  tfrcllembxssdm  6026  ltexnqq  6730  enq0tr  6756  prarloc  6825  addclpr  6859  nqprxx  6868  mulclpr  6894  ltexprlempr  6930  recexprlempr  6954  cauappcvgprlemcl  6975  caucvgprlemcl  6998  caucvgprprlemcl  7026  le2tri3i  7356  ltmul1  7829  nn0ge2m1nn  8485  nn0ge0div  8585  eluzp1p1  8795  peano2uz  8822  ledivge1le  8954  elioc2  9105  elico2  9106  elicc2  9107  iccsupr  9135  uzsubsubfz  9212  fzrev3  9250  elfz1b  9253  fseq1p1m1  9257  elfz0ubfz0  9283  elfz0fzfz0  9284  fz0fzelfz0  9285  fz0fzdiffz0  9288  elfzmlbp  9290  elfzo2  9307  elfzo0  9338  fzo1fzo0n0  9339  elfzo0z  9340  fzofzim  9344  elfzo1  9346  ubmelfzo  9356  elfzodifsumelfzo  9357  elfzom1elp1fzo  9358  fzossfzop1  9368  ssfzo12bi  9381  subfzo0  9398  fldiv4p1lem1div2  9457  intqfrac2  9471  intfracq  9472  modfzo0difsn  9547  remullem  9977  qdenre  10307  maxabslemval  10313  divconjdvds  10475  addmodlteqALT  10485  ltoddhalfle  10518  4dvdseven  10542  dfgcd2  10628  rppwr  10642  qredeq  10703  divgcdcoprmex  10709  cncongr1  10710  dvdsnprmd  10732  oddprmge3  10741
  Copyright terms: Public domain W3C validator