Theorem 3jca 1208

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

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

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 1011

This theorem is referenced by:  3jcad  1209  mpbir3and  1211  syl3anbrc  1212  3anim123i  1215  syl3anc  1278  syl13anc  1280  syl31anc  1281  syl113anc  1290  syl131anc  1291  syl311anc  1292  syl33anc  1293  syl133anc  1301  syl313anc  1302  syl331anc  1303  syl333anc  1310  3jaob  1343  mp3and  1381  issod  4459  fvun1d  5765  fvun2d  5766  funsssuppss  6488  tfrlemibxssdm  6588  tfr1onlembxssdm  6604  tfrcllembxssdm  6617  ctssdccl  7441  onntri35  7586  dftap2  7607  ltexnqq  7765  enq0tr  7791  prarloc  7860  addclpr  7894  nqprxx  7903  mulclpr  7929  ltexprlempr  7965  recexprlempr  7989  cauappcvgprlemcl  8010  caucvgprlemcl  8033  caucvgprprlemcl  8061  suplocexprlemex  8079  mpomulf  8306  le2tri3i  8424  ltmul1  8910  nn0ge2m1nn  9606  difgtsumgt  9693  nn0ge0div  9712  eluzp1p1  9927  peano2uz  9962  zgt1rpn0n1  10075  ledivge1le  10106  elioc2  10317  elico2  10318  elicc2  10319  iccsupr  10347  elfzd  10398  uzsubsubfz  10430  fzrev3  10472  elfz1b  10475  fseq1p1m1  10479  elfz0ubfz0  10510  elfz0fzfz0  10511  fz0fzelfz0  10512  fz0fzdiffz0  10515  elfzmlbp  10517  elfzo2  10535  elfzo0  10571  nn0p1elfzo  10572  fzo1fzo0n0  10573  elfzo0z  10574  fzofzim  10578  elfzo1  10581  ubmelfzo  10596  elfzodifsumelfzo  10597  elfzom1elp1fzo  10598  fzossfzop1  10608  ssfzo12bi  10621  subfzo0  10639  fldiv4p1lem1div2  10718  intqfrac2  10734  intfracq  10735  modfzo0difsn  10810  iseqf1olemqcl  10914  iseqf1olemnab  10916  iseqf1olemab  10917  seq3f1olemqsumkj  10926  seq3f1olemqsumk  10927  seq3f1olemstep  10929  seqf1oglem2  10935  hashtpg  11277  wrdlenge2n0  11318  ccatval21sw  11351  ccatass  11354  lswccatn0lsw  11357  wrdl1s1  11376  swrdlen2  11412  swrdfv2  11413  swrdspsleq  11417  swrdccat2  11421  pfxnd  11439  swrdswrdlem  11454  swrdpfx  11457  pfxpfx  11458  pfxccatin12lem2a  11477  pfxccatin12lem1  11478  swrdccatin2  11479  pfxccatin12lem2c  11480  pfxccatin12lem2  11481  pfxccatin12lem3  11482  pfxccatin12  11483  pfxccat3  11484  swrdccat  11485  remullem  11614  qdenre  11946  maxabslemval  11952  xrmaxiflemval  11994  summodclem2a  12126  fsum3  12132  fsum3cvg3  12141  fsumcl2lem  12143  fsumadd  12151  sumsplitdc  12177  fsummulc2  12193  isumlessdc  12241  prodmodclem3  12320  prodmodclem2a  12321  prodmodclem2  12322  prodmodc  12323  fprodeq0  12362  sin02gt0  12509  p1modz1  12539  divconjdvds  12594  addmodlteqALT  12604  ltoddhalfle  12638  4dvdseven  12662  dfgcd2  12769  rppwr  12783  qredeq  12852  divgcdcoprmex  12858  cncongr1  12859  dvdsnprmd  12881  oddprmge3  12891  isprm5  12898  pythagtriplem6  13027  pythagtriplem7  13028  pythagtriplem19  13039  difsqpwdvds  13095  oddprmdvds  13111  ennnfoneleminc  13280  ctinf  13299  ssomct  13314  sgrpidmndm  13710  idmhm  13753  mhmf1o  13754  insubm  13769  0mhm  13770  resmhm  13771  resmhm2  13772  resmhm2b  13773  mhmco  13774  grpinvid1  13834  grpinvid2  13835  grplcan  13844  dfgrp3m  13881  dfgrp3me  13882  mhmfmhm  13897  issubg2m  13969  issubg4m  13973  ghmmhm  14033  rngrz  14220  srglmhm  14271  srgrmhm  14272  ringlz  14321  ringrz  14322  ringinvnzdiv  14328  ring1  14337  unitgrp  14396  isrhm2d  14445  subrgunit  14520  issubrg2  14522  islmodd  14602  dflidl2rng  14790  rnglidlmmgm  14805  quscrng  14842  upxp  15296  bdmopn  15528  suplociccex  15649  ivthreinc  15669  ptolemy  15848  perfectlem1  16027  gausslemma2dlem1a  16091  gausslemma2dlem4  16097  uhgr2edg  16361  umgrvad2edg  16366  uspgredg2vlem  16375  wlkpropg  16479  wlkv  16481  wlkvtxeledgg  16499  upgr2wlkdc  16532  trlsv  16539  clwwlkccat  16556  umgrclwwlkge2  16557  loopclwwlkn1b  16574  clwwlkn1loopb  16575  clwwlkext2edg  16577  s2elclwwlknon2  16591  clwwlknonex2lem2  16593  clwwlknonex2  16594  eupthv  16601  depindlem1  16661  dceqnconst  17015  dcapnconst  17016