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  4466  fvun1d  5774  fvun2d  5775  funsssuppss  6502  tfrlemibxssdm  6603  tfr1onlembxssdm  6619  tfrcllembxssdm  6632  ctssdccl  7457  onntri35  7602  dftap2  7623  ltexnqq  7781  enq0tr  7807  prarloc  7876  addclpr  7910  nqprxx  7919  mulclpr  7945  ltexprlempr  7981  recexprlempr  8005  cauappcvgprlemcl  8026  caucvgprlemcl  8049  caucvgprprlemcl  8077  suplocexprlemex  8095  mpomulf  8322  le2tri3i  8441  ltmul1  8928  nn0ge2m1nn  9636  difgtsumgt  9723  nn0ge0div  9742  eluzp1p1  9963  peano2uz  9998  zgt1rpn0n1  10112  ledivge1le  10143  elioc2  10354  elico2  10355  elicc2  10356  iccsupr  10384  elfzd  10435  uzsubsubfz  10468  fzrev3  10510  elfz1b  10513  fseq1p1m1  10517  elfz0ubfz0  10548  elfz0fzfz0  10549  fz0fzelfz0  10550  fz0fzdiffz0  10553  elfzmlbp  10555  elfzo2  10573  elfzo0  10609  nn0p1elfzo  10610  fzo1fzo0n0  10611  elfzo0z  10612  fzofzim  10616  elfzo1  10619  ubmelfzo  10634  elfzodifsumelfzo  10635  elfzom1elp1fzo  10636  fzossfzop1  10646  ssfzo12bi  10659  subfzo0  10677  fldiv4p1lem1div2  10760  intqfrac2  10776  intfracq  10777  modfzo0difsn  10852  iseqf1olemqcl  10956  iseqf1olemnab  10958  iseqf1olemab  10959  seq3f1olemqsumkj  10968  seq3f1olemqsumk  10969  seq3f1olemstep  10971  seqf1oglem2  10977  hashtpg  11320  wrdlenge2n0  11361  ccatval21sw  11394  ccatass  11397  lswccatn0lsw  11400  wrdl1s1  11419  swrdlen2  11455  swrdfv2  11456  swrdspsleq  11460  swrdccat2  11464  pfxnd  11482  swrdswrdlem  11497  swrdpfx  11500  pfxpfx  11501  pfxccatin12lem2a  11520  pfxccatin12lem1  11521  swrdccatin2  11522  pfxccatin12lem2c  11523  pfxccatin12lem2  11524  pfxccatin12lem3  11525  pfxccatin12  11526  pfxccat3  11527  swrdccat  11528  remullem  11657  qdenre  11990  maxabslemval  11996  xrmaxiflemval  12040  summodclem2a  12172  fsum3  12178  fsum3cvg3  12187  fsumcl2lem  12189  fsumadd  12197  sumsplitdc  12223  fsummulc2  12239  isumlessdc  12287  prodmodclem3  12366  prodmodclem2a  12367  prodmodclem2  12368  prodmodc  12369  fprodeq0  12408  sin02gt0  12555  p1modz1  12585  divconjdvds  12640  addmodlteqALT  12650  ltoddhalfle  12684  4dvdseven  12708  dfgcd2  12815  rppwr  12829  qredeq  12898  divgcdcoprmex  12904  cncongr1  12905  dvdsnprmd  12927  oddprmge3  12938  isprm5  12945  pythagtriplem6  13077  pythagtriplem7  13078  pythagtriplem19  13089  difsqpwdvds  13145  oddprmdvds  13161  ennnfoneleminc  13359  ctinf  13378  ssomct  13393  sgrpidmndm  13791  idmhm  13834  mhmf1o  13835  insubm  13850  0mhm  13851  resmhm  13852  resmhm2  13853  resmhm2b  13854  mhmco  13855  grpinvid1  13915  grpinvid2  13916  grplcan  13925  dfgrp3m  13962  dfgrp3me  13963  mhmfmhm  13978  issubg2m  14050  issubg4m  14054  ghmmhm  14114  rngrz  14351  srglmhm  14403  srgrmhm  14404  ringlz  14454  ringrz  14455  ringinvnzdiv  14461  ring1  14470  unitgrp  14531  isrhm2d  14580  subrgunit  14655  issubrg2  14657  islmodd  14737  dflidl2rng  14926  rnglidlmmgm  14941  quscrng  14978  upxp  15515  bdmopn  15747  suplociccex  15868  ivthreinc  15888  ptolemy  16068  birthdaylem1g  16242  perfectlem1  16316  gausslemma2dlem1a  16399  gausslemma2dlem4  16405  uhgr2edg  16669  umgrvad2edg  16674  uspgredg2vlem  16683  wlkpropg  16787  wlkv  16789  wlkvtxeledgg  16807  upgr2wlkdc  16840  trlsv  16847  clwwlkccat  16864  umgrclwwlkge2  16865  loopclwwlkn1b  16882  clwwlkn1loopb  16883  clwwlkext2edg  16885  s2elclwwlknon2  16899  clwwlknonex2lem2  16901  clwwlknonex2  16902  eupthv  16909  depindlem1  16969  dceqnconst  17334  dcapnconst  17335