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  4410  tfrlemibxssdm  6479  tfr1onlembxssdm  6495  tfrcllembxssdm  6508  ctssdccl  7289  onntri35  7433  dftap2  7448  ltexnqq  7606  enq0tr  7632  prarloc  7701  addclpr  7735  nqprxx  7744  mulclpr  7770  ltexprlempr  7806  recexprlempr  7830  cauappcvgprlemcl  7851  caucvgprlemcl  7874  caucvgprprlemcl  7902  suplocexprlemex  7920  mpomulf  8147  le2tri3i  8266  ltmul1  8750  nn0ge2m1nn  9440  difgtsumgt  9527  nn0ge0div  9545  eluzp1p1  9760  peano2uz  9790  zgt1rpn0n1  9903  ledivge1le  9934  elioc2  10144  elico2  10145  elicc2  10146  iccsupr  10174  elfzd  10224  uzsubsubfz  10255  fzrev3  10295  elfz1b  10298  fseq1p1m1  10302  elfz0ubfz0  10333  elfz0fzfz0  10334  fz0fzelfz0  10335  fz0fzdiffz0  10338  elfzmlbp  10340  elfzo2  10358  elfzo0  10394  fzo1fzo0n0  10395  elfzo0z  10396  fzofzim  10400  elfzo1  10403  ubmelfzo  10418  elfzodifsumelfzo  10419  elfzom1elp1fzo  10420  fzossfzop1  10430  ssfzo12bi  10443  subfzo0  10460  fldiv4p1lem1div2  10537  intqfrac2  10553  intfracq  10554  modfzo0difsn  10629  iseqf1olemqcl  10733  iseqf1olemnab  10735  iseqf1olemab  10736  seq3f1olemqsumkj  10745  seq3f1olemqsumk  10746  seq3f1olemstep  10748  seqf1oglem2  10754  wrdlenge2n0  11120  ccatval21sw  11153  ccatass  11156  lswccatn0lsw  11159  wrdl1s1  11178  swrdlen2  11210  swrdfv2  11211  swrdspsleq  11215  swrdccat2  11219  pfxnd  11237  swrdswrdlem  11252  swrdpfx  11255  pfxpfx  11256  pfxccatin12lem2a  11275  pfxccatin12lem1  11276  swrdccatin2  11277  pfxccatin12lem2c  11278  pfxccatin12lem2  11279  pfxccatin12lem3  11280  pfxccatin12  11281  pfxccat3  11282  swrdccat  11283  remullem  11398  qdenre  11729  maxabslemval  11735  xrmaxiflemval  11777  summodclem2a  11908  fsum3  11914  fsum3cvg3  11923  fsumcl2lem  11925  fsumadd  11933  sumsplitdc  11959  fsummulc2  11975  isumlessdc  12023  prodmodclem3  12102  prodmodclem2a  12103  prodmodclem2  12104  prodmodc  12105  fprodeq0  12144  sin02gt0  12291  p1modz1  12321  divconjdvds  12376  addmodlteqALT  12386  ltoddhalfle  12420  4dvdseven  12444  dfgcd2  12551  rppwr  12565  qredeq  12634  divgcdcoprmex  12640  cncongr1  12641  dvdsnprmd  12663  oddprmge3  12673  isprm5  12680  pythagtriplem6  12809  pythagtriplem7  12810  pythagtriplem19  12821  difsqpwdvds  12877  oddprmdvds  12893  ennnfoneleminc  12998  ctinf  13017  ssomct  13032  sgrpidmndm  13469  idmhm  13518  mhmf1o  13519  insubm  13534  0mhm  13535  resmhm  13536  resmhm2  13537  resmhm2b  13538  mhmco  13539  grpinvid1  13601  grpinvid2  13602  grplcan  13611  dfgrp3m  13648  dfgrp3me  13649  mhmfmhm  13670  issubg2m  13742  issubg4m  13746  ghmmhm  13806  rngrz  13925  srglmhm  13972  srgrmhm  13973  ringlz  14022  ringrz  14023  ringinvnzdiv  14029  ring1  14038  unitgrp  14096  isrhm2d  14145  subrgunit  14219  issubrg2  14221  islmodd  14273  dflidl2rng  14461  rnglidlmmgm  14476  quscrng  14513  upxp  14962  bdmopn  15194  suplociccex  15315  ivthreinc  15335  ptolemy  15514  perfectlem1  15689  gausslemma2dlem1a  15753  gausslemma2dlem4  15759  uhgr2edg  16020  umgrvad2edg  16025  uspgredg2vlem  16034  wlkpropg  16070  wlkv  16072  wlkvtxeledgg  16090  upgr2wlkdc  16121  trlsv  16128  clwwlkccat  16144  umgrclwwlkge2  16145  loopclwwlkn1b  16161  clwwlkn1loopb  16162  clwwlkext2edg  16164  dceqnconst  16516  dcapnconst  16517