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 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used 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  4464  fvun1d  5771  fvun2d  5772  funsssuppss  6498  tfrlemibxssdm  6598  tfr1onlembxssdm  6614  tfrcllembxssdm  6627  ctssdccl  7451  onntri35  7596  dftap2  7617  ltexnqq  7775  enq0tr  7801  prarloc  7870  addclpr  7904  nqprxx  7913  mulclpr  7939  ltexprlempr  7975  recexprlempr  7999  cauappcvgprlemcl  8020  caucvgprlemcl  8043  caucvgprprlemcl  8071  suplocexprlemex  8089  mpomulf  8316  le2tri3i  8434  ltmul1  8920  nn0ge2m1nn  9627  difgtsumgt  9714  nn0ge0div  9733  eluzp1p1  9948  peano2uz  9983  zgt1rpn0n1  10096  ledivge1le  10127  elioc2  10338  elico2  10339  elicc2  10340  iccsupr  10368  elfzd  10419  uzsubsubfz  10452  fzrev3  10494  elfz1b  10497  fseq1p1m1  10501  elfz0ubfz0  10532  elfz0fzfz0  10533  fz0fzelfz0  10534  fz0fzdiffz0  10537  elfzmlbp  10539  elfzo2  10557  elfzo0  10593  nn0p1elfzo  10594  fzo1fzo0n0  10595  elfzo0z  10596  fzofzim  10600  elfzo1  10603  ubmelfzo  10618  elfzodifsumelfzo  10619  elfzom1elp1fzo  10620  fzossfzop1  10630  ssfzo12bi  10643  subfzo0  10661  fldiv4p1lem1div2  10740  intqfrac2  10756  intfracq  10757  modfzo0difsn  10832  iseqf1olemqcl  10936  iseqf1olemnab  10938  iseqf1olemab  10939  seq3f1olemqsumkj  10948  seq3f1olemqsumk  10949  seq3f1olemstep  10951  seqf1oglem2  10957  hashtpg  11299  wrdlenge2n0  11340  ccatval21sw  11373  ccatass  11376  lswccatn0lsw  11379  wrdl1s1  11398  swrdlen2  11434  swrdfv2  11435  swrdspsleq  11439  swrdccat2  11443  pfxnd  11461  swrdswrdlem  11476  swrdpfx  11479  pfxpfx  11480  pfxccatin12lem2a  11499  pfxccatin12lem1  11500  swrdccatin2  11501  pfxccatin12lem2c  11502  pfxccatin12lem2  11503  pfxccatin12lem3  11504  pfxccatin12  11505  pfxccat3  11506  swrdccat  11507  remullem  11636  qdenre  11968  maxabslemval  11974  xrmaxiflemval  12016  summodclem2a  12148  fsum3  12154  fsum3cvg3  12163  fsumcl2lem  12165  fsumadd  12173  sumsplitdc  12199  fsummulc2  12215  isumlessdc  12263  prodmodclem3  12342  prodmodclem2a  12343  prodmodclem2  12344  prodmodc  12345  fprodeq0  12384  sin02gt0  12531  p1modz1  12561  divconjdvds  12616  addmodlteqALT  12626  ltoddhalfle  12660  4dvdseven  12684  dfgcd2  12791  rppwr  12805  qredeq  12874  divgcdcoprmex  12880  cncongr1  12881  dvdsnprmd  12903  oddprmge3  12913  isprm5  12920  pythagtriplem6  13049  pythagtriplem7  13050  pythagtriplem19  13061  difsqpwdvds  13117  oddprmdvds  13133  ennnfoneleminc  13302  ctinf  13321  ssomct  13336  sgrpidmndm  13733  idmhm  13776  mhmf1o  13777  insubm  13792  0mhm  13793  resmhm  13794  resmhm2  13795  resmhm2b  13796  mhmco  13797  grpinvid1  13857  grpinvid2  13858  grplcan  13867  dfgrp3m  13904  dfgrp3me  13905  mhmfmhm  13920  issubg2m  13992  issubg4m  13996  ghmmhm  14056  rngrz  14245  srglmhm  14297  srgrmhm  14298  ringlz  14348  ringrz  14349  ringinvnzdiv  14355  ring1  14364  unitgrp  14423  isrhm2d  14472  subrgunit  14547  issubrg2  14549  islmodd  14629  dflidl2rng  14818  rnglidlmmgm  14833  quscrng  14870  upxp  15373  bdmopn  15605  suplociccex  15726  ivthreinc  15746  ptolemy  15925  birthdaylem1g  16087  perfectlem1  16113  gausslemma2dlem1a  16177  gausslemma2dlem4  16183  uhgr2edg  16447  umgrvad2edg  16452  uspgredg2vlem  16461  wlkpropg  16565  wlkv  16567  wlkvtxeledgg  16585  upgr2wlkdc  16618  trlsv  16625  clwwlkccat  16642  umgrclwwlkge2  16643  loopclwwlkn1b  16660  clwwlkn1loopb  16661  clwwlkext2edg  16663  s2elclwwlknon2  16677  clwwlknonex2lem2  16679  clwwlknonex2  16680  eupthv  16687  depindlem1  16747  dceqnconst  17110  dcapnconst  17111