Theorem 3jca 1177

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

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

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 980

This theorem is referenced by:  3jcad  1178  mpbir3and  1180  syl3anbrc  1181  3anim123i  1184  syl3anc  1238  syl13anc  1240  syl31anc  1241  syl113anc  1250  syl131anc  1251  syl311anc  1252  syl33anc  1253  syl133anc  1261  syl313anc  1262  syl331anc  1263  syl333anc  1270  3jaob  1302  mp3and  1340  issod  4313  tfrlemibxssdm  6318  tfr1onlembxssdm  6334  tfrcllembxssdm  6347  ctssdccl  7100  onntri35  7226  ltexnqq  7382  enq0tr  7408  prarloc  7477  addclpr  7511  nqprxx  7520  mulclpr  7546  ltexprlempr  7582  recexprlempr  7606  cauappcvgprlemcl  7627  caucvgprlemcl  7650  caucvgprprlemcl  7678  suplocexprlemex  7696  le2tri3i  8040  ltmul1  8523  nn0ge2m1nn  9209  difgtsumgt  9295  nn0ge0div  9313  eluzp1p1  9526  peano2uz  9556  zgt1rpn0n1  9666  ledivge1le  9697  elioc2  9907  elico2  9908  elicc2  9909  iccsupr  9937  uzsubsubfz  10017  fzrev3  10057  elfz1b  10060  fseq1p1m1  10064  elfz0ubfz0  10095  elfz0fzfz0  10096  fz0fzelfz0  10097  fz0fzdiffz0  10100  elfzmlbp  10102  elfzo2  10120  elfzo0  10152  fzo1fzo0n0  10153  elfzo0z  10154  fzofzim  10158  elfzo1  10160  ubmelfzo  10170  elfzodifsumelfzo  10171  elfzom1elp1fzo  10172  fzossfzop1  10182  ssfzo12bi  10195  subfzo0  10212  fldiv4p1lem1div2  10275  intqfrac2  10289  intfracq  10290  modfzo0difsn  10365  iseqf1olemqcl  10456  iseqf1olemnab  10458  iseqf1olemab  10459  seq3f1olemqsumkj  10468  seq3f1olemqsumk  10469  seq3f1olemstep  10471  remullem  10848  qdenre  11179  maxabslemval  11185  xrmaxiflemval  11226  summodclem2a  11357  fsum3  11363  fsum3cvg3  11372  fsumcl2lem  11374  fsumadd  11382  sumsplitdc  11408  fsummulc2  11424  isumlessdc  11472  prodmodclem3  11551  prodmodclem2a  11552  prodmodclem2  11553  prodmodc  11554  fprodeq0  11593  sin02gt0  11739  p1modz1  11769  divconjdvds  11822  addmodlteqALT  11832  ltoddhalfle  11865  4dvdseven  11889  dfgcd2  11982  rppwr  11996  qredeq  12063  divgcdcoprmex  12069  cncongr1  12070  dvdsnprmd  12092  oddprmge3  12102  isprm5  12109  pythagtriplem6  12237  pythagtriplem7  12238  pythagtriplem19  12249  difsqpwdvds  12304  oddprmdvds  12319  ennnfoneleminc  12379  ctinf  12398  ssomct  12413  sgrpidmndm  12696  idmhm  12732  mhmf1o  12733  insubm  12743  0mhm  12744  mhmco  12745  grpinvid1  12795  grpinvid2  12796  grplcan  12802  dfgrp3m  12839  dfgrp3me  12840  mhmfmhm  12851  srglmhm  12982  srgrmhm  12983  ringlz  13027  ringrz  13028  ringinvnzdiv  13032  ring1  13041  upxp  13352  bdmopn  13584  suplociccex  13683  ptolemy  13825  dceqnconst  14377  dcapnconst  14378