Theorem 3jca 1179

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

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

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 982

This theorem is referenced by:  3jcad  1180  mpbir3and  1182  syl3anbrc  1183  3anim123i  1186  syl3anc  1249  syl13anc  1251  syl31anc  1252  syl113anc  1261  syl131anc  1262  syl311anc  1263  syl33anc  1264  syl133anc  1272  syl313anc  1273  syl331anc  1274  syl333anc  1281  3jaob  1313  mp3and  1351  issod  4337  tfrlemibxssdm  6353  tfr1onlembxssdm  6369  tfrcllembxssdm  6382  ctssdccl  7141  onntri35  7267  dftap2  7281  ltexnqq  7438  enq0tr  7464  prarloc  7533  addclpr  7567  nqprxx  7576  mulclpr  7602  ltexprlempr  7638  recexprlempr  7662  cauappcvgprlemcl  7683  caucvgprlemcl  7706  caucvgprprlemcl  7734  suplocexprlemex  7752  le2tri3i  8097  ltmul1  8580  nn0ge2m1nn  9267  difgtsumgt  9353  nn0ge0div  9371  eluzp1p1  9585  peano2uz  9615  zgt1rpn0n1  9727  ledivge1le  9758  elioc2  9968  elico2  9969  elicc2  9970  iccsupr  9998  elfzd  10048  uzsubsubfz  10079  fzrev3  10119  elfz1b  10122  fseq1p1m1  10126  elfz0ubfz0  10157  elfz0fzfz0  10158  fz0fzelfz0  10159  fz0fzdiffz0  10162  elfzmlbp  10164  elfzo2  10182  elfzo0  10214  fzo1fzo0n0  10215  elfzo0z  10216  fzofzim  10220  elfzo1  10222  ubmelfzo  10232  elfzodifsumelfzo  10233  elfzom1elp1fzo  10234  fzossfzop1  10244  ssfzo12bi  10257  subfzo0  10274  fldiv4p1lem1div2  10338  intqfrac2  10352  intfracq  10353  modfzo0difsn  10428  iseqf1olemqcl  10519  iseqf1olemnab  10521  iseqf1olemab  10522  seq3f1olemqsumkj  10531  seq3f1olemqsumk  10532  seq3f1olemstep  10534  remullem  10915  qdenre  11246  maxabslemval  11252  xrmaxiflemval  11293  summodclem2a  11424  fsum3  11430  fsum3cvg3  11439  fsumcl2lem  11441  fsumadd  11449  sumsplitdc  11475  fsummulc2  11491  isumlessdc  11539  prodmodclem3  11618  prodmodclem2a  11619  prodmodclem2  11620  prodmodc  11621  fprodeq0  11660  sin02gt0  11806  p1modz1  11836  divconjdvds  11890  addmodlteqALT  11900  ltoddhalfle  11933  4dvdseven  11957  dfgcd2  12050  rppwr  12064  qredeq  12131  divgcdcoprmex  12137  cncongr1  12138  dvdsnprmd  12160  oddprmge3  12170  isprm5  12177  pythagtriplem6  12305  pythagtriplem7  12306  pythagtriplem19  12317  difsqpwdvds  12373  oddprmdvds  12389  ennnfoneleminc  12465  ctinf  12484  ssomct  12499  sgrpidmndm  12896  idmhm  12936  mhmf1o  12937  insubm  12952  0mhm  12953  resmhm  12954  resmhm2  12955  resmhm2b  12956  mhmco  12957  grpinvid1  13011  grpinvid2  13012  grplcan  13021  dfgrp3m  13058  dfgrp3me  13059  mhmfmhm  13074  issubg2m  13145  issubg4m  13149  ghmmhm  13209  rngrz  13317  srglmhm  13364  srgrmhm  13365  ringlz  13414  ringrz  13415  ringinvnzdiv  13419  ring1  13428  unitgrp  13483  isrhm2d  13532  subrgunit  13603  issubrg2  13605  islmodd  13626  dflidl2rng  13814  rnglidlmmgm  13829  quscrng  13864  upxp  14249  bdmopn  14481  suplociccex  14580  ptolemy  14722  dceqnconst  15287  dcapnconst  15288