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  7353  onntri35  7498  dftap2  7513  ltexnqq  7671  enq0tr  7697  prarloc  7766  addclpr  7800  nqprxx  7809  mulclpr  7835  ltexprlempr  7871  recexprlempr  7895  cauappcvgprlemcl  7916  caucvgprlemcl  7939  caucvgprprlemcl  7967  suplocexprlemex  7985  mpomulf  8212  le2tri3i  8331  ltmul1  8815  nn0ge2m1nn  9505  difgtsumgt  9592  nn0ge0div  9610  eluzp1p1  9825  peano2uz  9860  zgt1rpn0n1  9973  ledivge1le  10004  elioc2  10214  elico2  10215  elicc2  10216  iccsupr  10244  elfzd  10294  uzsubsubfz  10325  fzrev3  10365  elfz1b  10368  fseq1p1m1  10372  elfz0ubfz0  10403  elfz0fzfz0  10404  fz0fzelfz0  10405  fz0fzdiffz0  10408  elfzmlbp  10410  elfzo2  10428  elfzo0  10464  nn0p1elfzo  10465  fzo1fzo0n0  10466  elfzo0z  10467  fzofzim  10471  elfzo1  10474  ubmelfzo  10489  elfzodifsumelfzo  10490  elfzom1elp1fzo  10491  fzossfzop1  10501  ssfzo12bi  10514  subfzo0  10532  fldiv4p1lem1div2  10609  intqfrac2  10625  intfracq  10626  modfzo0difsn  10701  iseqf1olemqcl  10805  iseqf1olemnab  10807  iseqf1olemab  10808  seq3f1olemqsumkj  10817  seq3f1olemqsumk  10818  seq3f1olemstep  10820  seqf1oglem2  10826  hashtpg  11155  wrdlenge2n0  11196  ccatval21sw  11229  ccatass  11232  lswccatn0lsw  11235  wrdl1s1  11254  swrdlen2  11290  swrdfv2  11291  swrdspsleq  11295  swrdccat2  11299  pfxnd  11317  swrdswrdlem  11332  swrdpfx  11335  pfxpfx  11336  pfxccatin12lem2a  11355  pfxccatin12lem1  11356  swrdccatin2  11357  pfxccatin12lem2c  11358  pfxccatin12lem2  11359  pfxccatin12lem3  11360  pfxccatin12  11361  pfxccat3  11362  swrdccat  11363  remullem  11492  qdenre  11823  maxabslemval  11829  xrmaxiflemval  11871  summodclem2a  12003  fsum3  12009  fsum3cvg3  12018  fsumcl2lem  12020  fsumadd  12028  sumsplitdc  12054  fsummulc2  12070  isumlessdc  12118  prodmodclem3  12197  prodmodclem2a  12198  prodmodclem2  12199  prodmodc  12200  fprodeq0  12239  sin02gt0  12386  p1modz1  12416  divconjdvds  12471  addmodlteqALT  12481  ltoddhalfle  12515  4dvdseven  12539  dfgcd2  12646  rppwr  12660  qredeq  12729  divgcdcoprmex  12735  cncongr1  12736  dvdsnprmd  12758  oddprmge3  12768  isprm5  12775  pythagtriplem6  12904  pythagtriplem7  12905  pythagtriplem19  12916  difsqpwdvds  12972  oddprmdvds  12988  ennnfoneleminc  13093  ctinf  13112  ssomct  13127  sgrpidmndm  13564  idmhm  13613  mhmf1o  13614  insubm  13629  0mhm  13630  resmhm  13631  resmhm2  13632  resmhm2b  13633  mhmco  13634  grpinvid1  13696  grpinvid2  13697  grplcan  13706  dfgrp3m  13743  dfgrp3me  13744  mhmfmhm  13765  issubg2m  13837  issubg4m  13841  ghmmhm  13901  rngrz  14021  srglmhm  14068  srgrmhm  14069  ringlz  14118  ringrz  14119  ringinvnzdiv  14125  ring1  14134  unitgrp  14192  isrhm2d  14241  subrgunit  14315  issubrg2  14317  islmodd  14369  dflidl2rng  14557  rnglidlmmgm  14572  quscrng  14609  upxp  15063  bdmopn  15295  suplociccex  15416  ivthreinc  15436  ptolemy  15615  perfectlem1  15793  gausslemma2dlem1a  15857  gausslemma2dlem4  15863  uhgr2edg  16127  umgrvad2edg  16132  uspgredg2vlem  16141  wlkpropg  16245  wlkv  16247  wlkvtxeledgg  16265  upgr2wlkdc  16298  trlsv  16305  clwwlkccat  16322  umgrclwwlkge2  16323  loopclwwlkn1b  16340  clwwlkn1loopb  16341  clwwlkext2edg  16343  s2elclwwlknon2  16357  clwwlknonex2lem2  16359  clwwlknonex2  16360  eupthv  16367  depindlem1  16427  dceqnconst  16773  dcapnconst  16774