Theorem 3jca 1180

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

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

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 983

This theorem is referenced by:  3jcad  1181  mpbir3and  1183  syl3anbrc  1184  3anim123i  1187  syl3anc  1250  syl13anc  1252  syl31anc  1253  syl113anc  1262  syl131anc  1263  syl311anc  1264  syl33anc  1265  syl133anc  1273  syl313anc  1274  syl331anc  1275  syl333anc  1282  3jaob  1315  mp3and  1353  issod  4366  tfrlemibxssdm  6413  tfr1onlembxssdm  6429  tfrcllembxssdm  6442  ctssdccl  7213  onntri35  7349  dftap2  7363  ltexnqq  7521  enq0tr  7547  prarloc  7616  addclpr  7650  nqprxx  7659  mulclpr  7685  ltexprlempr  7721  recexprlempr  7745  cauappcvgprlemcl  7766  caucvgprlemcl  7789  caucvgprprlemcl  7817  suplocexprlemex  7835  mpomulf  8062  le2tri3i  8181  ltmul1  8665  nn0ge2m1nn  9355  difgtsumgt  9442  nn0ge0div  9460  eluzp1p1  9674  peano2uz  9704  zgt1rpn0n1  9817  ledivge1le  9848  elioc2  10058  elico2  10059  elicc2  10060  iccsupr  10088  elfzd  10138  uzsubsubfz  10169  fzrev3  10209  elfz1b  10212  fseq1p1m1  10216  elfz0ubfz0  10247  elfz0fzfz0  10248  fz0fzelfz0  10249  fz0fzdiffz0  10252  elfzmlbp  10254  elfzo2  10272  elfzo0  10306  fzo1fzo0n0  10307  elfzo0z  10308  fzofzim  10312  elfzo1  10314  ubmelfzo  10329  elfzodifsumelfzo  10330  elfzom1elp1fzo  10331  fzossfzop1  10341  ssfzo12bi  10354  subfzo0  10371  fldiv4p1lem1div2  10448  intqfrac2  10464  intfracq  10465  modfzo0difsn  10540  iseqf1olemqcl  10644  iseqf1olemnab  10646  iseqf1olemab  10647  seq3f1olemqsumkj  10656  seq3f1olemqsumk  10657  seq3f1olemstep  10659  seqf1oglem2  10665  wrdlenge2n0  11029  ccatval21sw  11061  ccatass  11064  lswccatn0lsw  11067  wrdl1s1  11084  swrdlen2  11115  swrdfv2  11116  swrdspsleq  11120  swrdccat2  11124  remullem  11182  qdenre  11513  maxabslemval  11519  xrmaxiflemval  11561  summodclem2a  11692  fsum3  11698  fsum3cvg3  11707  fsumcl2lem  11709  fsumadd  11717  sumsplitdc  11743  fsummulc2  11759  isumlessdc  11807  prodmodclem3  11886  prodmodclem2a  11887  prodmodclem2  11888  prodmodc  11889  fprodeq0  11928  sin02gt0  12075  p1modz1  12105  divconjdvds  12160  addmodlteqALT  12170  ltoddhalfle  12204  4dvdseven  12228  dfgcd2  12335  rppwr  12349  qredeq  12418  divgcdcoprmex  12424  cncongr1  12425  dvdsnprmd  12447  oddprmge3  12457  isprm5  12464  pythagtriplem6  12593  pythagtriplem7  12594  pythagtriplem19  12605  difsqpwdvds  12661  oddprmdvds  12677  ennnfoneleminc  12782  ctinf  12801  ssomct  12816  sgrpidmndm  13252  idmhm  13301  mhmf1o  13302  insubm  13317  0mhm  13318  resmhm  13319  resmhm2  13320  resmhm2b  13321  mhmco  13322  grpinvid1  13384  grpinvid2  13385  grplcan  13394  dfgrp3m  13431  dfgrp3me  13432  mhmfmhm  13453  issubg2m  13525  issubg4m  13529  ghmmhm  13589  rngrz  13708  srglmhm  13755  srgrmhm  13756  ringlz  13805  ringrz  13806  ringinvnzdiv  13812  ring1  13821  unitgrp  13878  isrhm2d  13927  subrgunit  14001  issubrg2  14003  islmodd  14055  dflidl2rng  14243  rnglidlmmgm  14258  quscrng  14295  upxp  14744  bdmopn  14976  suplociccex  15097  ivthreinc  15117  ptolemy  15296  perfectlem1  15471  gausslemma2dlem1a  15535  gausslemma2dlem4  15541  dceqnconst  15999  dcapnconst  16000