Theorem 3jca 1204

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

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

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 1007

This theorem is referenced by:  3jcad  1205  mpbir3and  1207  syl3anbrc  1208  3anim123i  1211  syl3anc  1274  syl13anc  1276  syl31anc  1277  syl113anc  1286  syl131anc  1287  syl311anc  1288  syl33anc  1289  syl133anc  1297  syl313anc  1298  syl331anc  1299  syl333anc  1306  3jaob  1339  mp3and  1377  issod  4440  funsssuppss  6458  tfrlemibxssdm  6558  tfr1onlembxssdm  6574  tfrcllembxssdm  6587  ctssdccl  7402  onntri35  7547  dftap2  7565  ltexnqq  7723  enq0tr  7749  prarloc  7818  addclpr  7852  nqprxx  7861  mulclpr  7887  ltexprlempr  7923  recexprlempr  7947  cauappcvgprlemcl  7968  caucvgprlemcl  7991  caucvgprprlemcl  8019  suplocexprlemex  8037  mpomulf  8264  le2tri3i  8382  ltmul1  8866  nn0ge2m1nn  9560  difgtsumgt  9647  nn0ge0div  9665  eluzp1p1  9880  peano2uz  9915  zgt1rpn0n1  10028  ledivge1le  10059  elioc2  10269  elico2  10270  elicc2  10271  iccsupr  10299  elfzd  10350  uzsubsubfz  10381  fzrev3  10421  elfz1b  10424  fseq1p1m1  10428  elfz0ubfz0  10459  elfz0fzfz0  10460  fz0fzelfz0  10461  fz0fzdiffz0  10464  elfzmlbp  10466  elfzo2  10484  elfzo0  10520  nn0p1elfzo  10521  fzo1fzo0n0  10522  elfzo0z  10523  fzofzim  10527  elfzo1  10530  ubmelfzo  10545  elfzodifsumelfzo  10546  elfzom1elp1fzo  10547  fzossfzop1  10557  ssfzo12bi  10570  subfzo0  10588  fldiv4p1lem1div2  10665  intqfrac2  10681  intfracq  10682  modfzo0difsn  10757  iseqf1olemqcl  10861  iseqf1olemnab  10863  iseqf1olemab  10864  seq3f1olemqsumkj  10873  seq3f1olemqsumk  10874  seq3f1olemstep  10876  seqf1oglem2  10882  hashtpg  11219  wrdlenge2n0  11260  ccatval21sw  11293  ccatass  11296  lswccatn0lsw  11299  wrdl1s1  11318  swrdlen2  11354  swrdfv2  11355  swrdspsleq  11359  swrdccat2  11363  pfxnd  11381  swrdswrdlem  11396  swrdpfx  11399  pfxpfx  11400  pfxccatin12lem2a  11419  pfxccatin12lem1  11420  swrdccatin2  11421  pfxccatin12lem2c  11422  pfxccatin12lem2  11423  pfxccatin12lem3  11424  pfxccatin12  11425  pfxccat3  11426  swrdccat  11427  remullem  11556  qdenre  11887  maxabslemval  11893  xrmaxiflemval  11935  summodclem2a  12067  fsum3  12073  fsum3cvg3  12082  fsumcl2lem  12084  fsumadd  12092  sumsplitdc  12118  fsummulc2  12134  isumlessdc  12182  prodmodclem3  12261  prodmodclem2a  12262  prodmodclem2  12263  prodmodc  12264  fprodeq0  12303  sin02gt0  12450  p1modz1  12480  divconjdvds  12535  addmodlteqALT  12545  ltoddhalfle  12579  4dvdseven  12603  dfgcd2  12710  rppwr  12724  qredeq  12793  divgcdcoprmex  12799  cncongr1  12800  dvdsnprmd  12822  oddprmge3  12832  isprm5  12839  pythagtriplem6  12968  pythagtriplem7  12969  pythagtriplem19  12980  difsqpwdvds  13036  oddprmdvds  13052  ennnfoneleminc  13162  ctinf  13181  ssomct  13196  sgrpidmndm  13633  idmhm  13682  mhmf1o  13683  insubm  13698  0mhm  13699  resmhm  13700  resmhm2  13701  resmhm2b  13702  mhmco  13703  grpinvid1  13765  grpinvid2  13766  grplcan  13775  dfgrp3m  13812  dfgrp3me  13813  mhmfmhm  13834  issubg2m  13906  issubg4m  13910  ghmmhm  13970  rngrz  14090  srglmhm  14137  srgrmhm  14138  ringlz  14187  ringrz  14188  ringinvnzdiv  14194  ring1  14203  unitgrp  14261  isrhm2d  14310  subrgunit  14384  issubrg2  14386  islmodd  14441  dflidl2rng  14629  rnglidlmmgm  14644  quscrng  14681  upxp  15137  bdmopn  15369  suplociccex  15490  ivthreinc  15510  ptolemy  15689  perfectlem1  15867  gausslemma2dlem1a  15931  gausslemma2dlem4  15937  uhgr2edg  16201  umgrvad2edg  16206  uspgredg2vlem  16215  wlkpropg  16319  wlkv  16321  wlkvtxeledgg  16339  upgr2wlkdc  16372  trlsv  16379  clwwlkccat  16396  umgrclwwlkge2  16397  loopclwwlkn1b  16414  clwwlkn1loopb  16415  clwwlkext2edg  16417  s2elclwwlknon2  16431  clwwlknonex2lem2  16433  clwwlknonex2  16434  eupthv  16441  depindlem1  16501  dceqnconst  16846  dcapnconst  16847