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  4422  funsssuppss  6436  tfrlemibxssdm  6536  tfr1onlembxssdm  6552  tfrcllembxssdm  6565  ctssdccl  7370  onntri35  7515  dftap2  7530  ltexnqq  7688  enq0tr  7714  prarloc  7783  addclpr  7817  nqprxx  7826  mulclpr  7852  ltexprlempr  7888  recexprlempr  7912  cauappcvgprlemcl  7933  caucvgprlemcl  7956  caucvgprprlemcl  7984  suplocexprlemex  8002  mpomulf  8229  le2tri3i  8347  ltmul1  8831  nn0ge2m1nn  9523  difgtsumgt  9610  nn0ge0div  9628  eluzp1p1  9843  peano2uz  9878  zgt1rpn0n1  9991  ledivge1le  10022  elioc2  10232  elico2  10233  elicc2  10234  iccsupr  10262  elfzd  10313  uzsubsubfz  10344  fzrev3  10384  elfz1b  10387  fseq1p1m1  10391  elfz0ubfz0  10422  elfz0fzfz0  10423  fz0fzelfz0  10424  fz0fzdiffz0  10427  elfzmlbp  10429  elfzo2  10447  elfzo0  10483  nn0p1elfzo  10484  fzo1fzo0n0  10485  elfzo0z  10486  fzofzim  10490  elfzo1  10493  ubmelfzo  10508  elfzodifsumelfzo  10509  elfzom1elp1fzo  10510  fzossfzop1  10520  ssfzo12bi  10533  subfzo0  10551  fldiv4p1lem1div2  10628  intqfrac2  10644  intfracq  10645  modfzo0difsn  10720  iseqf1olemqcl  10824  iseqf1olemnab  10826  iseqf1olemab  10827  seq3f1olemqsumkj  10836  seq3f1olemqsumk  10837  seq3f1olemstep  10839  seqf1oglem2  10845  hashtpg  11174  wrdlenge2n0  11215  ccatval21sw  11248  ccatass  11251  lswccatn0lsw  11254  wrdl1s1  11273  swrdlen2  11309  swrdfv2  11310  swrdspsleq  11314  swrdccat2  11318  pfxnd  11336  swrdswrdlem  11351  swrdpfx  11354  pfxpfx  11355  pfxccatin12lem2a  11374  pfxccatin12lem1  11375  swrdccatin2  11376  pfxccatin12lem2c  11377  pfxccatin12lem2  11378  pfxccatin12lem3  11379  pfxccatin12  11380  pfxccat3  11381  swrdccat  11382  remullem  11511  qdenre  11842  maxabslemval  11848  xrmaxiflemval  11890  summodclem2a  12022  fsum3  12028  fsum3cvg3  12037  fsumcl2lem  12039  fsumadd  12047  sumsplitdc  12073  fsummulc2  12089  isumlessdc  12137  prodmodclem3  12216  prodmodclem2a  12217  prodmodclem2  12218  prodmodc  12219  fprodeq0  12258  sin02gt0  12405  p1modz1  12435  divconjdvds  12490  addmodlteqALT  12500  ltoddhalfle  12534  4dvdseven  12558  dfgcd2  12665  rppwr  12679  qredeq  12748  divgcdcoprmex  12754  cncongr1  12755  dvdsnprmd  12777  oddprmge3  12787  isprm5  12794  pythagtriplem6  12923  pythagtriplem7  12924  pythagtriplem19  12935  difsqpwdvds  12991  oddprmdvds  13007  ennnfoneleminc  13112  ctinf  13131  ssomct  13146  sgrpidmndm  13583  idmhm  13632  mhmf1o  13633  insubm  13648  0mhm  13649  resmhm  13650  resmhm2  13651  resmhm2b  13652  mhmco  13653  grpinvid1  13715  grpinvid2  13716  grplcan  13725  dfgrp3m  13762  dfgrp3me  13763  mhmfmhm  13784  issubg2m  13856  issubg4m  13860  ghmmhm  13920  rngrz  14040  srglmhm  14087  srgrmhm  14088  ringlz  14137  ringrz  14138  ringinvnzdiv  14144  ring1  14153  unitgrp  14211  isrhm2d  14260  subrgunit  14334  issubrg2  14336  islmodd  14389  dflidl2rng  14577  rnglidlmmgm  14592  quscrng  14629  upxp  15083  bdmopn  15315  suplociccex  15436  ivthreinc  15456  ptolemy  15635  perfectlem1  15813  gausslemma2dlem1a  15877  gausslemma2dlem4  15883  uhgr2edg  16147  umgrvad2edg  16152  uspgredg2vlem  16161  wlkpropg  16265  wlkv  16267  wlkvtxeledgg  16285  upgr2wlkdc  16318  trlsv  16325  clwwlkccat  16342  umgrclwwlkge2  16343  loopclwwlkn1b  16360  clwwlkn1loopb  16361  clwwlkext2edg  16363  s2elclwwlknon2  16377  clwwlknonex2lem2  16379  clwwlknonex2  16380  eupthv  16387  depindlem1  16447  dceqnconst  16793  dcapnconst  16794