ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3jca Structured version   GIF 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  6416  prarloc  6485  addclpr  6519  nqprxx  6528  mulclpr  6552  ltexprlempr  6581  recexprlempr  6603  cauappcvgprlemcl  6624  le2tri3i  6903  ltmul1  7356  nn0ge2m1nn  7998  nn0ge0div  8083  eluzp1p1  8254  peano2uz  8282  elioc2  8555  elico2  8556  elicc2  8557  iccsupr  8585  uzsubsubfz  8661  fzrev3  8699  elfz1b  8702  fseq1p1m1  8706  elfz0ubfz0  8732  elfz0fzfz0  8733  fz0fzelfz0  8734  fz0fzdiffz0  8737  elfzmlbmOLD  8739  elfzmlbp  8740  elfzo2  8757  elfzo0  8788  fzo1fzo0n0  8789  elfzo0z  8790  fzofzim  8794  elfzo1  8796  ubmelfzo  8806  elfzodifsumelfzo  8807  elfzom1elp1fzo  8808  fzossfzop1  8818  ssfzo12bi  8831  remullem  9079
  Copyright terms: Public domain W3C validator