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

Theorem 3jca 1161
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 307 . 2 (𝜑 → ((𝜓𝜒) ∧ 𝜃))
5 df-3an 964 . 2 ((𝜓𝜒𝜃) ↔ ((𝜓𝜒) ∧ 𝜃))
64, 5sylibr 133 1 (𝜑 → (𝜓𝜒𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 962
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 964
This theorem is referenced by:  3jcad  1162  mpbir3and  1164  syl3anbrc  1165  3anim123i  1166  syl3anc  1216  syl13anc  1218  syl31anc  1219  syl113anc  1228  syl131anc  1229  syl311anc  1230  syl33anc  1231  syl133anc  1239  syl313anc  1240  syl331anc  1241  syl333anc  1248  3jaob  1280  mp3and  1318  issod  4241  tfrlemibxssdm  6224  tfr1onlembxssdm  6240  tfrcllembxssdm  6253  ctssdccl  6996  ltexnqq  7230  enq0tr  7256  prarloc  7325  addclpr  7359  nqprxx  7368  mulclpr  7394  ltexprlempr  7430  recexprlempr  7454  cauappcvgprlemcl  7475  caucvgprlemcl  7498  caucvgprprlemcl  7526  suplocexprlemex  7544  le2tri3i  7886  ltmul1  8368  nn0ge2m1nn  9051  nn0ge0div  9152  eluzp1p1  9365  peano2uz  9392  ledivge1le  9527  elioc2  9733  elico2  9734  elicc2  9735  iccsupr  9763  uzsubsubfz  9841  fzrev3  9881  elfz1b  9884  fseq1p1m1  9888  elfz0ubfz0  9916  elfz0fzfz0  9917  fz0fzelfz0  9918  fz0fzdiffz0  9921  elfzmlbp  9923  elfzo2  9941  elfzo0  9973  fzo1fzo0n0  9974  elfzo0z  9975  fzofzim  9979  elfzo1  9981  ubmelfzo  9991  elfzodifsumelfzo  9992  elfzom1elp1fzo  9993  fzossfzop1  10003  ssfzo12bi  10016  subfzo0  10033  fldiv4p1lem1div2  10092  intqfrac2  10106  intfracq  10107  modfzo0difsn  10182  iseqf1olemqcl  10273  iseqf1olemnab  10275  iseqf1olemab  10276  seq3f1olemqsumkj  10285  seq3f1olemqsumk  10286  seq3f1olemstep  10288  remullem  10657  qdenre  10988  maxabslemval  10994  xrmaxiflemval  11033  summodclem2a  11164  fsum3  11170  fsum3cvg3  11179  fsumcl2lem  11181  fsumadd  11189  sumsplitdc  11215  fsummulc2  11231  isumlessdc  11279  prodmodclem3  11358  prodmodclem2a  11359  prodmodclem2  11360  prodmodc  11361  sin02gt0  11483  divconjdvds  11560  addmodlteqALT  11570  ltoddhalfle  11603  4dvdseven  11627  dfgcd2  11715  rppwr  11729  qredeq  11790  divgcdcoprmex  11796  cncongr1  11797  dvdsnprmd  11819  oddprmge3  11828  ennnfoneleminc  11937  ctinf  11956  upxp  12457  bdmopn  12689  suplociccex  12788  ptolemy  12929
  Copyright terms: Public domain W3C validator