Theorem 3jca 1201

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 1004	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜓 ∧ 𝜒) ∧ 𝜃))
6	4, 5	sylibr 134	1 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))

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

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 1004

This theorem is referenced by:  3jcad  1202  mpbir3and  1204  syl3anbrc  1205  3anim123i  1208  syl3anc  1271  syl13anc  1273  syl31anc  1274  syl113anc  1283  syl131anc  1284  syl311anc  1285  syl33anc  1286  syl133anc  1294  syl313anc  1295  syl331anc  1296  syl333anc  1303  3jaob  1336  mp3and  1374  issod  4414  tfrlemibxssdm  6488  tfr1onlembxssdm  6504  tfrcllembxssdm  6517  ctssdccl  7301  onntri35  7445  dftap2  7460  ltexnqq  7618  enq0tr  7644  prarloc  7713  addclpr  7747  nqprxx  7756  mulclpr  7782  ltexprlempr  7818  recexprlempr  7842  cauappcvgprlemcl  7863  caucvgprlemcl  7886  caucvgprprlemcl  7914  suplocexprlemex  7932  mpomulf  8159  le2tri3i  8278  ltmul1  8762  nn0ge2m1nn  9452  difgtsumgt  9539  nn0ge0div  9557  eluzp1p1  9772  peano2uz  9807  zgt1rpn0n1  9920  ledivge1le  9951  elioc2  10161  elico2  10162  elicc2  10163  iccsupr  10191  elfzd  10241  uzsubsubfz  10272  fzrev3  10312  elfz1b  10315  fseq1p1m1  10319  elfz0ubfz0  10350  elfz0fzfz0  10351  fz0fzelfz0  10352  fz0fzdiffz0  10355  elfzmlbp  10357  elfzo2  10375  elfzo0  10411  fzo1fzo0n0  10412  elfzo0z  10413  fzofzim  10417  elfzo1  10420  ubmelfzo  10435  elfzodifsumelfzo  10436  elfzom1elp1fzo  10437  fzossfzop1  10447  ssfzo12bi  10460  subfzo0  10478  fldiv4p1lem1div2  10555  intqfrac2  10571  intfracq  10572  modfzo0difsn  10647  iseqf1olemqcl  10751  iseqf1olemnab  10753  iseqf1olemab  10754  seq3f1olemqsumkj  10763  seq3f1olemqsumk  10764  seq3f1olemstep  10766  seqf1oglem2  10772  wrdlenge2n0  11139  ccatval21sw  11172  ccatass  11175  lswccatn0lsw  11178  wrdl1s1  11197  swrdlen2  11233  swrdfv2  11234  swrdspsleq  11238  swrdccat2  11242  pfxnd  11260  swrdswrdlem  11275  swrdpfx  11278  pfxpfx  11279  pfxccatin12lem2a  11298  pfxccatin12lem1  11299  swrdccatin2  11300  pfxccatin12lem2c  11301  pfxccatin12lem2  11302  pfxccatin12lem3  11303  pfxccatin12  11304  pfxccat3  11305  swrdccat  11306  remullem  11422  qdenre  11753  maxabslemval  11759  xrmaxiflemval  11801  summodclem2a  11932  fsum3  11938  fsum3cvg3  11947  fsumcl2lem  11949  fsumadd  11957  sumsplitdc  11983  fsummulc2  11999  isumlessdc  12047  prodmodclem3  12126  prodmodclem2a  12127  prodmodclem2  12128  prodmodc  12129  fprodeq0  12168  sin02gt0  12315  p1modz1  12345  divconjdvds  12400  addmodlteqALT  12410  ltoddhalfle  12444  4dvdseven  12468  dfgcd2  12575  rppwr  12589  qredeq  12658  divgcdcoprmex  12664  cncongr1  12665  dvdsnprmd  12687  oddprmge3  12697  isprm5  12704  pythagtriplem6  12833  pythagtriplem7  12834  pythagtriplem19  12845  difsqpwdvds  12901  oddprmdvds  12917  ennnfoneleminc  13022  ctinf  13041  ssomct  13056  sgrpidmndm  13493  idmhm  13542  mhmf1o  13543  insubm  13558  0mhm  13559  resmhm  13560  resmhm2  13561  resmhm2b  13562  mhmco  13563  grpinvid1  13625  grpinvid2  13626  grplcan  13635  dfgrp3m  13672  dfgrp3me  13673  mhmfmhm  13694  issubg2m  13766  issubg4m  13770  ghmmhm  13830  rngrz  13949  srglmhm  13996  srgrmhm  13997  ringlz  14046  ringrz  14047  ringinvnzdiv  14053  ring1  14062  unitgrp  14120  isrhm2d  14169  subrgunit  14243  issubrg2  14245  islmodd  14297  dflidl2rng  14485  rnglidlmmgm  14500  quscrng  14537  upxp  14986  bdmopn  15218  suplociccex  15339  ivthreinc  15359  ptolemy  15538  perfectlem1  15713  gausslemma2dlem1a  15777  gausslemma2dlem4  15783  uhgr2edg  16045  umgrvad2edg  16050  uspgredg2vlem  16059  wlkpropg  16121  wlkv  16123  wlkvtxeledgg  16141  upgr2wlkdc  16172  trlsv  16179  clwwlkccat  16196  umgrclwwlkge2  16197  loopclwwlkn1b  16214  clwwlkn1loopb  16215  clwwlkext2edg  16217  s2elclwwlknon2  16231  clwwlknonex2lem2  16233  clwwlknonex2  16234  eupthv  16241  dceqnconst  16600  dcapnconst  16601