Theorem 3jca 1201

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

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

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 1004

This theorem is referenced by:  3jcad  1202  mpbir3and  1204  syl3anbrc  1205  3anim123i  1208  syl3anc  1271  syl13anc  1273  syl31anc  1274  syl113anc  1283  syl131anc  1284  syl311anc  1285  syl33anc  1286  syl133anc  1294  syl313anc  1295  syl331anc  1296  syl333anc  1303  3jaob  1336  mp3and  1374  issod  4410  tfrlemibxssdm  6473  tfr1onlembxssdm  6489  tfrcllembxssdm  6502  ctssdccl  7278  onntri35  7422  dftap2  7437  ltexnqq  7595  enq0tr  7621  prarloc  7690  addclpr  7724  nqprxx  7733  mulclpr  7759  ltexprlempr  7795  recexprlempr  7819  cauappcvgprlemcl  7840  caucvgprlemcl  7863  caucvgprprlemcl  7891  suplocexprlemex  7909  mpomulf  8136  le2tri3i  8255  ltmul1  8739  nn0ge2m1nn  9429  difgtsumgt  9516  nn0ge0div  9534  eluzp1p1  9748  peano2uz  9778  zgt1rpn0n1  9891  ledivge1le  9922  elioc2  10132  elico2  10133  elicc2  10134  iccsupr  10162  elfzd  10212  uzsubsubfz  10243  fzrev3  10283  elfz1b  10286  fseq1p1m1  10290  elfz0ubfz0  10321  elfz0fzfz0  10322  fz0fzelfz0  10323  fz0fzdiffz0  10326  elfzmlbp  10328  elfzo2  10346  elfzo0  10382  fzo1fzo0n0  10383  elfzo0z  10384  fzofzim  10388  elfzo1  10391  ubmelfzo  10406  elfzodifsumelfzo  10407  elfzom1elp1fzo  10408  fzossfzop1  10418  ssfzo12bi  10431  subfzo0  10448  fldiv4p1lem1div2  10525  intqfrac2  10541  intfracq  10542  modfzo0difsn  10617  iseqf1olemqcl  10721  iseqf1olemnab  10723  iseqf1olemab  10724  seq3f1olemqsumkj  10733  seq3f1olemqsumk  10734  seq3f1olemstep  10736  seqf1oglem2  10742  wrdlenge2n0  11107  ccatval21sw  11140  ccatass  11143  lswccatn0lsw  11146  wrdl1s1  11163  swrdlen2  11194  swrdfv2  11195  swrdspsleq  11199  swrdccat2  11203  pfxnd  11221  swrdswrdlem  11236  swrdpfx  11239  pfxpfx  11240  pfxccatin12lem2a  11259  pfxccatin12lem1  11260  swrdccatin2  11261  pfxccatin12lem2c  11262  pfxccatin12lem2  11263  pfxccatin12lem3  11264  pfxccatin12  11265  pfxccat3  11266  swrdccat  11267  remullem  11382  qdenre  11713  maxabslemval  11719  xrmaxiflemval  11761  summodclem2a  11892  fsum3  11898  fsum3cvg3  11907  fsumcl2lem  11909  fsumadd  11917  sumsplitdc  11943  fsummulc2  11959  isumlessdc  12007  prodmodclem3  12086  prodmodclem2a  12087  prodmodclem2  12088  prodmodc  12089  fprodeq0  12128  sin02gt0  12275  p1modz1  12305  divconjdvds  12360  addmodlteqALT  12370  ltoddhalfle  12404  4dvdseven  12428  dfgcd2  12535  rppwr  12549  qredeq  12618  divgcdcoprmex  12624  cncongr1  12625  dvdsnprmd  12647  oddprmge3  12657  isprm5  12664  pythagtriplem6  12793  pythagtriplem7  12794  pythagtriplem19  12805  difsqpwdvds  12861  oddprmdvds  12877  ennnfoneleminc  12982  ctinf  13001  ssomct  13016  sgrpidmndm  13453  idmhm  13502  mhmf1o  13503  insubm  13518  0mhm  13519  resmhm  13520  resmhm2  13521  resmhm2b  13522  mhmco  13523  grpinvid1  13585  grpinvid2  13586  grplcan  13595  dfgrp3m  13632  dfgrp3me  13633  mhmfmhm  13654  issubg2m  13726  issubg4m  13730  ghmmhm  13790  rngrz  13909  srglmhm  13956  srgrmhm  13957  ringlz  14006  ringrz  14007  ringinvnzdiv  14013  ring1  14022  unitgrp  14080  isrhm2d  14129  subrgunit  14203  issubrg2  14205  islmodd  14257  dflidl2rng  14445  rnglidlmmgm  14460  quscrng  14497  upxp  14946  bdmopn  15178  suplociccex  15299  ivthreinc  15319  ptolemy  15498  perfectlem1  15673  gausslemma2dlem1a  15737  gausslemma2dlem4  15743  uhgr2edg  16004  umgrvad2edg  16009  uspgredg2vlem  16018  wlkpropg  16037  wlkv  16038  wlkvtxeledgg  16055  dceqnconst  16428  dcapnconst  16429