Theorem 3jca 1084

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

Step	Hyp	Ref	Expression
1		3jca.1	. . 3 |- ( ph -> ps )
2		3jca.2	. . 3 |- ( ph -> ch )
3		3jca.3	. . 3 |- ( ph -> th )
4	1, 2, 3	jca31 292	. 2 |- ( ph -> ( ( ps /\ ch ) /\ th ) )
5		df-3an 887	. 2 |- ( ( ps /\ ch /\ th ) <-> ( ( ps /\ ch ) /\ th ) )
6	4, 5	sylibr 137	1 |- ( ph -> ( ps /\ ch /\ th ) )

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  6506  enq0tr  6532  prarloc  6601  addclpr  6635  nqprxx  6644  mulclpr  6670  ltexprlempr  6706  recexprlempr  6730  cauappcvgprlemcl  6751  caucvgprlemcl  6774  caucvgprprlemcl  6802  le2tri3i  7126  ltmul1  7583  nn0ge2m1nn  8242  nn0ge0div  8327  eluzp1p1  8498  peano2uz  8526  ledivge1le  8652  elioc2  8805  elico2  8806  elicc2  8807  iccsupr  8835  uzsubsubfz  8911  fzrev3  8949  elfz1b  8952  fseq1p1m1  8956  elfz0ubfz0  8982  elfz0fzfz0  8983  fz0fzelfz0  8984  fz0fzdiffz0  8987  elfzmlbmOLD  8989  elfzmlbp  8990  elfzo2  9007  elfzo0  9038  fzo1fzo0n0  9039  elfzo0z  9040  fzofzim  9044  elfzo1  9046  ubmelfzo  9056  elfzodifsumelfzo  9057  elfzom1elp1fzo  9058  fzossfzop1  9068  ssfzo12bi  9081  subfzo0  9097  fldiv4p1lem1div2  9147  intqfrac2  9161  intfracq  9162  remullem  9471  qdenre  9798