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

Theorem 3jca 1084
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 887 . 2 ((𝜓𝜒𝜃) ↔ ((𝜓𝜒) ∧ 𝜃))
64, 5sylibr 137 1 (𝜑 → (𝜓𝜒𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97  w3a 885
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 887
This theorem is referenced by:  3jcad  1085  mpbir3and  1087  syl3anbrc  1088  3anim123i  1089  syl3anc  1135  syl13anc  1137  syl31anc  1138  syl113anc  1147  syl131anc  1148  syl311anc  1149  syl33anc  1150  syl133anc  1158  syl313anc  1159  syl331anc  1160  syl333anc  1167  3jaob  1197  issod  4056  tfrlemibxssdm  5941  ltexnqq  6504  enq0tr  6530  prarloc  6599  addclpr  6633  nqprxx  6642  mulclpr  6668  ltexprlempr  6704  recexprlempr  6728  cauappcvgprlemcl  6749  caucvgprlemcl  6772  caucvgprprlemcl  6800  le2tri3i  7124  ltmul1  7581  nn0ge2m1nn  8240  nn0ge0div  8325  eluzp1p1  8496  peano2uz  8524  ledivge1le  8650  elioc2  8803  elico2  8804  elicc2  8805  iccsupr  8833  uzsubsubfz  8909  fzrev3  8947  elfz1b  8950  fseq1p1m1  8954  elfz0ubfz0  8980  elfz0fzfz0  8981  fz0fzelfz0  8982  fz0fzdiffz0  8985  elfzmlbmOLD  8987  elfzmlbp  8988  elfzo2  9005  elfzo0  9036  fzo1fzo0n0  9037  elfzo0z  9038  fzofzim  9042  elfzo1  9044  ubmelfzo  9054  elfzodifsumelfzo  9055  elfzom1elp1fzo  9056  fzossfzop1  9066  ssfzo12bi  9079  subfzo0  9095  fldiv4p1lem1div2  9145  intqfrac2  9159  intfracq  9160  remullem  9469  qdenre  9796
  Copyright terms: Public domain W3C validator