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  7452  onntri35  7597  dftap2  7618  ltexnqq  7776  enq0tr  7802  prarloc  7871  addclpr  7905  nqprxx  7914  mulclpr  7940  ltexprlempr  7976  recexprlempr  8000  cauappcvgprlemcl  8021  caucvgprlemcl  8044  caucvgprprlemcl  8072  suplocexprlemex  8090  mpomulf  8317  le2tri3i  8436  ltmul1  8923  nn0ge2m1nn  9632  difgtsumgt  9719  nn0ge0div  9738  eluzp1p1  9958  peano2uz  9993  zgt1rpn0n1  10107  ledivge1le  10138  elioc2  10349  elico2  10350  elicc2  10351  iccsupr  10379  elfzd  10430  uzsubsubfz  10463  fzrev3  10505  elfz1b  10508  fseq1p1m1  10512  elfz0ubfz0  10543  elfz0fzfz0  10544  fz0fzelfz0  10545  fz0fzdiffz0  10548  elfzmlbp  10550  elfzo2  10568  elfzo0  10604  nn0p1elfzo  10605  fzo1fzo0n0  10606  elfzo0z  10607  fzofzim  10611  elfzo1  10614  ubmelfzo  10629  elfzodifsumelfzo  10630  elfzom1elp1fzo  10631  fzossfzop1  10641  ssfzo12bi  10654  subfzo0  10672  fldiv4p1lem1div2  10755  intqfrac2  10771  intfracq  10772  modfzo0difsn  10847  iseqf1olemqcl  10951  iseqf1olemnab  10953  iseqf1olemab  10954  seq3f1olemqsumkj  10963  seq3f1olemqsumk  10964  seq3f1olemstep  10966  seqf1oglem2  10972  hashtpg  11315  wrdlenge2n0  11356  ccatval21sw  11389  ccatass  11392  lswccatn0lsw  11395  wrdl1s1  11414  swrdlen2  11450  swrdfv2  11451  swrdspsleq  11455  swrdccat2  11459  pfxnd  11477  swrdswrdlem  11492  swrdpfx  11495  pfxpfx  11496  pfxccatin12lem2a  11515  pfxccatin12lem1  11516  swrdccatin2  11517  pfxccatin12lem2c  11518  pfxccatin12lem2  11519  pfxccatin12lem3  11520  pfxccatin12  11521  pfxccat3  11522  swrdccat  11523  remullem  11652  qdenre  11985  maxabslemval  11991  xrmaxiflemval  12035  summodclem2a  12167  fsum3  12173  fsum3cvg3  12182  fsumcl2lem  12184  fsumadd  12192  sumsplitdc  12218  fsummulc2  12234  isumlessdc  12282  prodmodclem3  12361  prodmodclem2a  12362  prodmodclem2  12363  prodmodc  12364  fprodeq0  12403  sin02gt0  12550  p1modz1  12580  divconjdvds  12635  addmodlteqALT  12645  ltoddhalfle  12679  4dvdseven  12703  dfgcd2  12810  rppwr  12824  qredeq  12893  divgcdcoprmex  12899  cncongr1  12900  dvdsnprmd  12922  oddprmge3  12933  isprm5  12940  pythagtriplem6  13072  pythagtriplem7  13073  pythagtriplem19  13084  difsqpwdvds  13140  oddprmdvds  13156  ennnfoneleminc  13354  ctinf  13373  ssomct  13388  sgrpidmndm  13786  idmhm  13829  mhmf1o  13830  insubm  13845  0mhm  13846  resmhm  13847  resmhm2  13848  resmhm2b  13849  mhmco  13850  grpinvid1  13910  grpinvid2  13911  grplcan  13920  dfgrp3m  13957  dfgrp3me  13958  mhmfmhm  13973  issubg2m  14045  issubg4m  14049  ghmmhm  14109  rngrz  14329  srglmhm  14381  srgrmhm  14382  ringlz  14432  ringrz  14433  ringinvnzdiv  14439  ring1  14448  unitgrp  14507  isrhm2d  14556  subrgunit  14631  issubrg2  14633  islmodd  14713  dflidl2rng  14902  rnglidlmmgm  14917  quscrng  14954  upxp  15464  bdmopn  15696  suplociccex  15817  ivthreinc  15837  ptolemy  16017  birthdaylem1g  16186  perfectlem1  16260  gausslemma2dlem1a  16343  gausslemma2dlem4  16349  uhgr2edg  16613  umgrvad2edg  16618  uspgredg2vlem  16627  wlkpropg  16731  wlkv  16733  wlkvtxeledgg  16751  upgr2wlkdc  16784  trlsv  16791  clwwlkccat  16808  umgrclwwlkge2  16809  loopclwwlkn1b  16826  clwwlkn1loopb  16827  clwwlkext2edg  16829  s2elclwwlknon2  16843  clwwlknonex2lem2  16845  clwwlknonex2  16846  eupthv  16853  depindlem1  16913  dceqnconst  17277  dcapnconst  17278