Theorem jca32 515

Description: Join three consequents. (Contributed by FL, 1-Aug-2009.)

Hypotheses

Ref	Expression
jca31.1	⊢ (𝜑 → 𝜓)
jca31.2	⊢ (𝜑 → 𝜒)
jca31.3	⊢ (𝜑 → 𝜃)

Assertion

Ref	Expression
jca32	⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃)))

Proof of Theorem jca32

Step	Hyp	Ref	Expression
1		jca31.1	. 2 ⊢ (𝜑 → 𝜓)
2		jca31.2	. . 3 ⊢ (𝜑 → 𝜒)
3		jca31.3	. . 3 ⊢ (𝜑 → 𝜃)
4	2, 3	jca 511	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
5	1, 4	jca 511	1 ⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  reuan  3834  domssl  8945  domssr  8946  sbthlem9  9033  nqerf  10853  lemul12a  12013  lediv12a  12049  elfzd  13469  fzass4  13516  4fvwrd4  13602  leexp1a  14137  wrd2ind  14685  cshwidxm1  14769  rtrclreclem4  15023  coprmproddvdslem  16631  reumodprminv  16775  prmgaplem6  17027  mreexexlem2d  17611  sgrp2nmndlem4  18899  pmtrrn2  19435  rngcinv  20614  ringcinv  20648  islmodd  20861  nn0srg  21417  rge0srg  21418  mdet1  22566  cpmatmcllem  22683  neitr  23145  restnlly  23447  llyrest  23450  llyidm  23453  uptx  23590  alexsubALTlem2  24013  alexsubALTlem4  24015  distspace  24281  ncvs1  25124  ivthlem3  25420  conway  27771  uzsind  28397  renegscl  28490  readdscl  28491  remulscl  28494  axtg5seg  28533  colperpexlem3  28800  outpasch  28823  iscgra1  28878  f1otrg  28939  ax5seg  29007  axcontlem4  29036  eengtrkg  29055  wlkonwlk1l  29730  crctcshwlkn0  29889  wwlksnextinj  29967  wwlksnextsurj  29968  clwwlkf1  30119  clwwlknon1  30167  numclwwlk1lem2f1  30427  wlkl0  30437  grpoidinv  30579  pjnmopi  32219  cdj1i  32504  xrofsup  32840  ccfldsrarelvec  33815  dya2iocnrect  34425  omssubadd  34444  sitgfval  34485  bnj969  35088  bnj1463  35197  erdszelem7  35379  rellysconn  35433  segconeq  36192  ifscgr  36226  btwnconn1lem13  36281  btwnconn1lem14  36282  outsideofeq  36312  ellines  36334  fnessref  36539  refssfne  36540  knoppndvlem14  36785  isbasisrelowllem1  37671  isbasisrelowllem2  37672  relowlssretop  37679  itg2gt0cn  37996  frinfm  38056  heiborlem3  38134  isfldidl  38389  eldisjs6  39261  4atlem12  40058  cdleme48fv  40945  cdlemg35  41159  mapd0  42111  aks4d1p1p5  42514  flt4lem7  43092  nna4b4nsq  43093  3cubeslem1  43116  mzpincl  43166  mzpindd  43178  diophin  43204  pellexlem3  43259  pellexlem5  43261  dfno2  43855  amgm3d  44626  amgm4d  44627  lptre2pt  46068  dvnprodlem2  46375  stoweidlem1  46429  stoweidlem14  46442  stoweidlem17  46445  stoweidlem27  46455  stoweidlem57  46485  fourierdlem12  46547  fourierdlem14  46549  fourierdlem70  46604  fourierdlem92  46626  fourierdlem111  46645  etransclem10  46672  etransclem24  46686  salgenval  46749  smfaddlem1  47191  f1cof1blem  47522  elfzelfzlble  47769  reuopreuprim  47986  gpgedgvtx0  48537  rngcinvALTV  48752  ringcinvALTV  48786  lmod1  48968  inlinecirc02plem  49262  nelsubclem  49542  oppf1st2nd  49606