Theorem 3jca 1203

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

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

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 1006

This theorem is referenced by:  3jcad  1204  mpbir3and  1206  syl3anbrc  1207  3anim123i  1210  syl3anc  1273  syl13anc  1275  syl31anc  1276  syl113anc  1285  syl131anc  1286  syl311anc  1287  syl33anc  1288  syl133anc  1296  syl313anc  1297  syl331anc  1298  syl333anc  1305  3jaob  1338  mp3and  1376  issod  4416  tfrlemibxssdm  6493  tfr1onlembxssdm  6509  tfrcllembxssdm  6522  ctssdccl  7310  onntri35  7455  dftap2  7470  ltexnqq  7628  enq0tr  7654  prarloc  7723  addclpr  7757  nqprxx  7766  mulclpr  7792  ltexprlempr  7828  recexprlempr  7852  cauappcvgprlemcl  7873  caucvgprlemcl  7896  caucvgprprlemcl  7924  suplocexprlemex  7942  mpomulf  8169  le2tri3i  8288  ltmul1  8772  nn0ge2m1nn  9462  difgtsumgt  9549  nn0ge0div  9567  eluzp1p1  9782  peano2uz  9817  zgt1rpn0n1  9930  ledivge1le  9961  elioc2  10171  elico2  10172  elicc2  10173  iccsupr  10201  elfzd  10251  uzsubsubfz  10282  fzrev3  10322  elfz1b  10325  fseq1p1m1  10329  elfz0ubfz0  10360  elfz0fzfz0  10361  fz0fzelfz0  10362  fz0fzdiffz0  10365  elfzmlbp  10367  elfzo2  10385  elfzo0  10421  nn0p1elfzo  10422  fzo1fzo0n0  10423  elfzo0z  10424  fzofzim  10428  elfzo1  10431  ubmelfzo  10446  elfzodifsumelfzo  10447  elfzom1elp1fzo  10448  fzossfzop1  10458  ssfzo12bi  10471  subfzo0  10489  fldiv4p1lem1div2  10566  intqfrac2  10582  intfracq  10583  modfzo0difsn  10658  iseqf1olemqcl  10762  iseqf1olemnab  10764  iseqf1olemab  10765  seq3f1olemqsumkj  10774  seq3f1olemqsumk  10775  seq3f1olemstep  10777  seqf1oglem2  10783  hashtpg  11112  wrdlenge2n0  11153  ccatval21sw  11186  ccatass  11189  lswccatn0lsw  11192  wrdl1s1  11211  swrdlen2  11247  swrdfv2  11248  swrdspsleq  11252  swrdccat2  11256  pfxnd  11274  swrdswrdlem  11289  swrdpfx  11292  pfxpfx  11293  pfxccatin12lem2a  11312  pfxccatin12lem1  11313  swrdccatin2  11314  pfxccatin12lem2c  11315  pfxccatin12lem2  11316  pfxccatin12lem3  11317  pfxccatin12  11318  pfxccat3  11319  swrdccat  11320  remullem  11449  qdenre  11780  maxabslemval  11786  xrmaxiflemval  11828  summodclem2a  11960  fsum3  11966  fsum3cvg3  11975  fsumcl2lem  11977  fsumadd  11985  sumsplitdc  12011  fsummulc2  12027  isumlessdc  12075  prodmodclem3  12154  prodmodclem2a  12155  prodmodclem2  12156  prodmodc  12157  fprodeq0  12196  sin02gt0  12343  p1modz1  12373  divconjdvds  12428  addmodlteqALT  12438  ltoddhalfle  12472  4dvdseven  12496  dfgcd2  12603  rppwr  12617  qredeq  12686  divgcdcoprmex  12692  cncongr1  12693  dvdsnprmd  12715  oddprmge3  12725  isprm5  12732  pythagtriplem6  12861  pythagtriplem7  12862  pythagtriplem19  12873  difsqpwdvds  12929  oddprmdvds  12945  ennnfoneleminc  13050  ctinf  13069  ssomct  13084  sgrpidmndm  13521  idmhm  13570  mhmf1o  13571  insubm  13586  0mhm  13587  resmhm  13588  resmhm2  13589  resmhm2b  13590  mhmco  13591  grpinvid1  13653  grpinvid2  13654  grplcan  13663  dfgrp3m  13700  dfgrp3me  13701  mhmfmhm  13722  issubg2m  13794  issubg4m  13798  ghmmhm  13858  rngrz  13978  srglmhm  14025  srgrmhm  14026  ringlz  14075  ringrz  14076  ringinvnzdiv  14082  ring1  14091  unitgrp  14149  isrhm2d  14198  subrgunit  14272  issubrg2  14274  islmodd  14326  dflidl2rng  14514  rnglidlmmgm  14529  quscrng  14566  upxp  15015  bdmopn  15247  suplociccex  15368  ivthreinc  15388  ptolemy  15567  perfectlem1  15742  gausslemma2dlem1a  15806  gausslemma2dlem4  15812  uhgr2edg  16076  umgrvad2edg  16081  uspgredg2vlem  16090  wlkpropg  16194  wlkv  16196  wlkvtxeledgg  16214  upgr2wlkdc  16247  trlsv  16254  clwwlkccat  16271  umgrclwwlkge2  16272  loopclwwlkn1b  16289  clwwlkn1loopb  16290  clwwlkext2edg  16292  s2elclwwlknon2  16306  clwwlknonex2lem2  16308  clwwlknonex2  16309  eupthv  16316  depindlem1  16376  dceqnconst  16716  dcapnconst  16717