Theorem 3jca 1161

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 307	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃))
5		df-3an 964	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) ↔ ((𝜓 ∧ 𝜒) ∧ 𝜃))
6	4, 5	sylibr 133	1 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  3jcad  1162  mpbir3and  1164  syl3anbrc  1165  3anim123i  1166  syl3anc  1216  syl13anc  1218  syl31anc  1219  syl113anc  1228  syl131anc  1229  syl311anc  1230  syl33anc  1231  syl133anc  1239  syl313anc  1240  syl331anc  1241  syl333anc  1248  3jaob  1280  mp3and  1318  issod  4236  tfrlemibxssdm  6217  tfr1onlembxssdm  6233  tfrcllembxssdm  6246  ctssdccl  6989  ltexnqq  7209  enq0tr  7235  prarloc  7304  addclpr  7338  nqprxx  7347  mulclpr  7373  ltexprlempr  7409  recexprlempr  7433  cauappcvgprlemcl  7454  caucvgprlemcl  7477  caucvgprprlemcl  7505  suplocexprlemex  7523  le2tri3i  7865  ltmul1  8347  nn0ge2m1nn  9030  nn0ge0div  9131  eluzp1p1  9344  peano2uz  9371  ledivge1le  9506  elioc2  9712  elico2  9713  elicc2  9714  iccsupr  9742  uzsubsubfz  9820  fzrev3  9860  elfz1b  9863  fseq1p1m1  9867  elfz0ubfz0  9895  elfz0fzfz0  9896  fz0fzelfz0  9897  fz0fzdiffz0  9900  elfzmlbp  9902  elfzo2  9920  elfzo0  9952  fzo1fzo0n0  9953  elfzo0z  9954  fzofzim  9958  elfzo1  9960  ubmelfzo  9970  elfzodifsumelfzo  9971  elfzom1elp1fzo  9972  fzossfzop1  9982  ssfzo12bi  9995  subfzo0  10012  fldiv4p1lem1div2  10071  intqfrac2  10085  intfracq  10086  modfzo0difsn  10161  iseqf1olemqcl  10252  iseqf1olemnab  10254  iseqf1olemab  10255  seq3f1olemqsumkj  10264  seq3f1olemqsumk  10265  seq3f1olemstep  10267  remullem  10636  qdenre  10967  maxabslemval  10973  xrmaxiflemval  11012  summodclem2a  11143  fsum3  11149  fsum3cvg3  11158  fsumcl2lem  11160  fsumadd  11168  sumsplitdc  11194  fsummulc2  11210  isumlessdc  11258  sin02gt0  11459  divconjdvds  11536  addmodlteqALT  11546  ltoddhalfle  11579  4dvdseven  11603  dfgcd2  11691  rppwr  11705  qredeq  11766  divgcdcoprmex  11772  cncongr1  11773  dvdsnprmd  11795  oddprmge3  11804  ennnfoneleminc  11913  ctinf  11932  upxp  12430  bdmopn  12662  suplociccex  12761  ptolemy  12894