Theorem 3jca 1177

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

Step	Hyp	Ref	Expression
1		3jca.1	. . 3 ⊢ (𝜑 → 𝜓)
2		3jca.2	. . 3 ⊢ (𝜑 → 𝜒)
3		3jca.3	. . 3 ⊢ (𝜑 → 𝜃)
4	1, 2, 3	jca31 309	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃))
5		df-3an 980	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜓 ∧ 𝜒) ∧ 𝜃))
6	4, 5	sylibr 134	1 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 978

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  3jcad  1178  mpbir3and  1180  syl3anbrc  1181  3anim123i  1184  syl3anc  1238  syl13anc  1240  syl31anc  1241  syl113anc  1250  syl131anc  1251  syl311anc  1252  syl33anc  1253  syl133anc  1261  syl313anc  1262  syl331anc  1263  syl333anc  1270  3jaob  1302  mp3and  1340  issod  4320  tfrlemibxssdm  6328  tfr1onlembxssdm  6344  tfrcllembxssdm  6357  ctssdccl  7110  onntri35  7236  dftap2  7250  ltexnqq  7407  enq0tr  7433  prarloc  7502  addclpr  7536  nqprxx  7545  mulclpr  7571  ltexprlempr  7607  recexprlempr  7631  cauappcvgprlemcl  7652  caucvgprlemcl  7675  caucvgprprlemcl  7703  suplocexprlemex  7721  le2tri3i  8066  ltmul1  8549  nn0ge2m1nn  9236  difgtsumgt  9322  nn0ge0div  9340  eluzp1p1  9553  peano2uz  9583  zgt1rpn0n1  9695  ledivge1le  9726  elioc2  9936  elico2  9937  elicc2  9938  iccsupr  9966  elfzd  10016  uzsubsubfz  10047  fzrev3  10087  elfz1b  10090  fseq1p1m1  10094  elfz0ubfz0  10125  elfz0fzfz0  10126  fz0fzelfz0  10127  fz0fzdiffz0  10130  elfzmlbp  10132  elfzo2  10150  elfzo0  10182  fzo1fzo0n0  10183  elfzo0z  10184  fzofzim  10188  elfzo1  10190  ubmelfzo  10200  elfzodifsumelfzo  10201  elfzom1elp1fzo  10202  fzossfzop1  10212  ssfzo12bi  10225  subfzo0  10242  fldiv4p1lem1div2  10305  intqfrac2  10319  intfracq  10320  modfzo0difsn  10395  iseqf1olemqcl  10486  iseqf1olemnab  10488  iseqf1olemab  10489  seq3f1olemqsumkj  10498  seq3f1olemqsumk  10499  seq3f1olemstep  10501  remullem  10880  qdenre  11211  maxabslemval  11217  xrmaxiflemval  11258  summodclem2a  11389  fsum3  11395  fsum3cvg3  11404  fsumcl2lem  11406  fsumadd  11414  sumsplitdc  11440  fsummulc2  11456  isumlessdc  11504  prodmodclem3  11583  prodmodclem2a  11584  prodmodclem2  11585  prodmodc  11586  fprodeq0  11625  sin02gt0  11771  p1modz1  11801  divconjdvds  11855  addmodlteqALT  11865  ltoddhalfle  11898  4dvdseven  11922  dfgcd2  12015  rppwr  12029  qredeq  12096  divgcdcoprmex  12102  cncongr1  12103  dvdsnprmd  12125  oddprmge3  12135  isprm5  12142  pythagtriplem6  12270  pythagtriplem7  12271  pythagtriplem19  12282  difsqpwdvds  12337  oddprmdvds  12352  ennnfoneleminc  12412  ctinf  12431  ssomct  12446  sgrpidmndm  12821  idmhm  12860  mhmf1o  12861  insubm  12872  0mhm  12873  mhmco  12874  grpinvid1  12924  grpinvid2  12925  grplcan  12932  dfgrp3m  12969  dfgrp3me  12970  mhmfmhm  12981  issubg2m  13049  issubg4m  13053  srglmhm  13176  srgrmhm  13177  ringlz  13222  ringrz  13223  ringinvnzdiv  13227  ring1  13236  unitgrp  13285  subrgunit  13360  issubrg2  13362  islmodd  13383  upxp  13775  bdmopn  14007  suplociccex  14106  ptolemy  14248  dceqnconst  14810  dcapnconst  14811