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  4351  tfrlemibxssdm  6382  tfr1onlembxssdm  6398  tfrcllembxssdm  6411  ctssdccl  7172  onntri35  7299  dftap2  7313  ltexnqq  7470  enq0tr  7496  prarloc  7565  addclpr  7599  nqprxx  7608  mulclpr  7634  ltexprlempr  7670  recexprlempr  7694  cauappcvgprlemcl  7715  caucvgprlemcl  7738  caucvgprprlemcl  7766  suplocexprlemex  7784  mpomulf  8011  le2tri3i  8130  ltmul1  8613  nn0ge2m1nn  9303  difgtsumgt  9389  nn0ge0div  9407  eluzp1p1  9621  peano2uz  9651  zgt1rpn0n1  9764  ledivge1le  9795  elioc2  10005  elico2  10006  elicc2  10007  iccsupr  10035  elfzd  10085  uzsubsubfz  10116  fzrev3  10156  elfz1b  10159  fseq1p1m1  10163  elfz0ubfz0  10194  elfz0fzfz0  10195  fz0fzelfz0  10196  fz0fzdiffz0  10199  elfzmlbp  10201  elfzo2  10219  elfzo0  10252  fzo1fzo0n0  10253  elfzo0z  10254  fzofzim  10258  elfzo1  10260  ubmelfzo  10270  elfzodifsumelfzo  10271  elfzom1elp1fzo  10272  fzossfzop1  10282  ssfzo12bi  10295  subfzo0  10312  fldiv4p1lem1div2  10377  intqfrac2  10393  intfracq  10394  modfzo0difsn  10469  iseqf1olemqcl  10573  iseqf1olemnab  10575  iseqf1olemab  10576  seq3f1olemqsumkj  10585  seq3f1olemqsumk  10586  seq3f1olemstep  10588  seqf1oglem2  10594  wrdlenge2n0  10952  remullem  11018  qdenre  11349  maxabslemval  11355  xrmaxiflemval  11396  summodclem2a  11527  fsum3  11533  fsum3cvg3  11542  fsumcl2lem  11544  fsumadd  11552  sumsplitdc  11578  fsummulc2  11594  isumlessdc  11642  prodmodclem3  11721  prodmodclem2a  11722  prodmodclem2  11723  prodmodc  11724  fprodeq0  11763  sin02gt0  11910  p1modz1  11940  divconjdvds  11994  addmodlteqALT  12004  ltoddhalfle  12037  4dvdseven  12061  dfgcd2  12154  rppwr  12168  qredeq  12237  divgcdcoprmex  12243  cncongr1  12244  dvdsnprmd  12266  oddprmge3  12276  isprm5  12283  pythagtriplem6  12411  pythagtriplem7  12412  pythagtriplem19  12423  difsqpwdvds  12479  oddprmdvds  12495  ennnfoneleminc  12571  ctinf  12590  ssomct  12605  sgrpidmndm  13004  idmhm  13044  mhmf1o  13045  insubm  13060  0mhm  13061  resmhm  13062  resmhm2  13063  resmhm2b  13064  mhmco  13065  grpinvid1  13127  grpinvid2  13128  grplcan  13137  dfgrp3m  13174  dfgrp3me  13175  mhmfmhm  13190  issubg2m  13262  issubg4m  13266  ghmmhm  13326  rngrz  13445  srglmhm  13492  srgrmhm  13493  ringlz  13542  ringrz  13543  ringinvnzdiv  13549  ring1  13558  unitgrp  13615  isrhm2d  13664  subrgunit  13738  issubrg2  13740  islmodd  13792  dflidl2rng  13980  rnglidlmmgm  13995  quscrng  14032  upxp  14451  bdmopn  14683  suplociccex  14804  ivthreinc  14824  ptolemy  15000  gausslemma2dlem1a  15215  gausslemma2dlem4  15221  dceqnconst  15620  dcapnconst  15621