Theorem 3jca 1118

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 302	. 2 |- ( ph -> ( ( ps /\ ch ) /\ th ) )
5		df-3an 921	. 2 |- ( ( ps /\ ch /\ th ) <-> ( ( ps /\ ch ) /\ th ) )
6	4, 5	sylibr 132	1 |- ( ph -> ( ps /\ ch /\ th ) )

Syntax hints:   -> wi 4   /\ wa 102   /\ w3a 919

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 921

This theorem is referenced by:  3jcad  1119  mpbir3and  1121  syl3anbrc  1122  3anim123i  1123  syl3anc  1169  syl13anc  1171  syl31anc  1172  syl113anc  1181  syl131anc  1182  syl311anc  1183  syl33anc  1184  syl133anc  1192  syl313anc  1193  syl331anc  1194  syl333anc  1201  3jaob  1233  mp3and  1271  issod  4074  tfrlemibxssdm  5964  ltexnqq  6598  enq0tr  6624  prarloc  6693  addclpr  6727  nqprxx  6736  mulclpr  6762  ltexprlempr  6798  recexprlempr  6822  cauappcvgprlemcl  6843  caucvgprlemcl  6866  caucvgprprlemcl  6894  le2tri3i  7219  ltmul1  7692  nn0ge2m1nn  8348  nn0ge0div  8434  eluzp1p1  8644  peano2uz  8671  ledivge1le  8803  elioc2  8959  elico2  8960  elicc2  8961  iccsupr  8989  uzsubsubfz  9066  fzrev3  9104  elfz1b  9107  fseq1p1m1  9111  elfz0ubfz0  9136  elfz0fzfz0  9137  fz0fzelfz0  9138  fz0fzdiffz0  9141  elfzmlbp  9143  elfzo2  9160  elfzo0  9191  fzo1fzo0n0  9192  elfzo0z  9193  fzofzim  9197  elfzo1  9199  ubmelfzo  9209  elfzodifsumelfzo  9210  elfzom1elp1fzo  9211  fzossfzop1  9221  ssfzo12bi  9234  subfzo0  9251  fldiv4p1lem1div2  9307  intqfrac2  9321  intfracq  9322  modfzo0difsn  9397  remullem  9758  qdenre  10088  maxabslemval  10094  divconjdvds  10249  addmodlteqALT  10259  ltoddhalfle  10293  4dvdseven  10317  dfgcd2  10403  rppwr  10417  qredeq  10478  divgcdcoprmex  10484  cncongr1  10485  dvdsnprmd  10507  oddprmge3  10516