Theorem 3jca 1126

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

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

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

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

This theorem is referenced by:  3jcad  1127  mpbir3and  1129  syl3anbrc  1130  3anim123i  1131  syl3anc  1181  syl13anc  1183  syl31anc  1184  syl113anc  1193  syl131anc  1194  syl311anc  1195  syl33anc  1196  syl133anc  1204  syl313anc  1205  syl331anc  1206  syl333anc  1213  3jaob  1245  mp3and  1283  issod  4170  tfrlemibxssdm  6130  tfr1onlembxssdm  6146  tfrcllembxssdm  6159  ltexnqq  7064  enq0tr  7090  prarloc  7159  addclpr  7193  nqprxx  7202  mulclpr  7228  ltexprlempr  7264  recexprlempr  7288  cauappcvgprlemcl  7309  caucvgprlemcl  7332  caucvgprprlemcl  7360  le2tri3i  7690  ltmul1  8166  nn0ge2m1nn  8831  nn0ge0div  8932  eluzp1p1  9143  peano2uz  9170  ledivge1le  9302  elioc2  9502  elico2  9503  elicc2  9504  iccsupr  9532  uzsubsubfz  9610  fzrev3  9650  elfz1b  9653  fseq1p1m1  9657  elfz0ubfz0  9685  elfz0fzfz0  9686  fz0fzelfz0  9687  fz0fzdiffz0  9690  elfzmlbp  9692  elfzo2  9710  elfzo0  9742  fzo1fzo0n0  9743  elfzo0z  9744  fzofzim  9748  elfzo1  9750  ubmelfzo  9760  elfzodifsumelfzo  9761  elfzom1elp1fzo  9762  fzossfzop1  9772  ssfzo12bi  9785  subfzo0  9802  fldiv4p1lem1div2  9861  intqfrac2  9875  intfracq  9876  modfzo0difsn  9951  iseqf1olemqcl  10052  iseqf1olemnab  10054  iseqf1olemab  10055  seq3f1olemqsumkj  10064  seq3f1olemqsumk  10065  seq3f1olemstep  10067  remullem  10436  qdenre  10766  maxabslemval  10772  xrmaxiflemval  10809  summodclem2a  10939  fsum3  10945  fsum3cvg3  10954  fsumcl2lem  10956  fsumadd  10964  sumsplitdc  10990  fsummulc2  11006  isumlessdc  11054  sin02gt0  11218  divconjdvds  11292  addmodlteqALT  11302  ltoddhalfle  11335  4dvdseven  11359  dfgcd2  11445  rppwr  11459  qredeq  11520  divgcdcoprmex  11526  cncongr1  11527  dvdsnprmd  11549  oddprmge3  11558  bdmopn  12305