Theorem jca32 524

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 520	. 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃))
5	1, 4	jca 520	1 ⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  reuan  3852  domssl  8983  domssr  8984  sbthlem9  9071  nqerf  10903  lemul12a  12061  lediv12a  12096  elfzd  13531  fzass4  13578  4fvwrd4  13664  leexp1a  14199  wrd2ind  14748  cshwidxm1  14832  rtrclreclem4  15086  coprmproddvdslem  16708  reumodprminv  16852  prmgaplem6  17104  mreexexlem2d  17689  sgrp2nmndlem4  18978  pmtrrn2  19518  rngcinv  20710  ringcinv  20744  islmodd  20953  nn0srg  21544  rge0srg  21545  mdet1  22715  cpmatmcllem  22832  neitr  23294  restnlly  23596  llyrest  23599  llyidm  23602  uptx  23739  alexsubALTlem2  24162  alexsubALTlem4  24164  distspace  24430  ncvs1  25273  ivthlem3  25569  conway  27926  uzsind  28552  renegscl  28645  readdscl  28646  remulscl  28649  axtg5seg  28688  tglnpt3  28877  colperpexlem3  28959  outpasch  28982  iscgra1  29058  f1otrg  29125  ax5seg  29193  axcontlem4  29222  eengtrkg  29241  wlkonwlk1l  29916  crctcshwlkn0  30075  wwlksnextinj  30153  wwlksnextsurj  30154  clwwlkf1  30305  clwwlknon1  30353  numclwwlk1lem2f1  30613  wlkl0  30623  grpoidinv  30765  pjnmopi  32405  cdj1i  32690  xrofsup  33020  ccfldsrarelvec  33973  dya2iocnrect  34583  omssubadd  34602  sitgfval  34643  bnj969  35246  bnj1463  35355  erdszelem7  35555  rellysconn  35609  segconeq  36368  ifscgr  36402  btwnconn1lem13  36457  btwnconn1lem14  36458  outsideofeq  36488  ellines  36510  fnessref  36725  refssfne  36726  knoppndvlem14  36971  isbasisrelowllem1  37856  isbasisrelowllem2  37857  relowlssretop  37864  itg2gt0cn  38181  frinfm  38241  heiborlem3  38319  isfldidl  38574  eldisjs6  39446  4atlem12  40243  cdleme48fv  41130  cdlemg35  41344  mapd0  42296  aks4d1p1p5  42699  flt4lem7  43248  nna4b4nsq  43249  3cubeslem1  43272  mzpincl  43322  mzpindd  43334  diophin  43360  pellexlem3  43415  pellexlem5  43417  dfno2  44011  amgm3d  44782  amgm4d  44783  lptre2pt  46213  dvnprodlem2  46520  stoweidlem1  46574  stoweidlem14  46587  stoweidlem17  46590  stoweidlem27  46600  stoweidlem57  46630  fourierdlem12  46692  fourierdlem14  46694  fourierdlem70  46749  fourierdlem92  46771  fourierdlem111  46790  etransclem10  46817  etransclem24  46831  salgenval  46894  smfaddlem1  47336  f1cof1blem  47667  elfzelfzlble  47914  reuopreuprim  48131  gpgedgvtx0  48682  rngcinvALTV  48897  ringcinvALTV  48931  lmod1  49124  inlinecirc02plem  49418  nelsubclem  49697  oppf1st2nd  49761