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 ⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401

This theorem is used by:  reuan  3849  domssl  8993  domssr  8994  sbthlem9  9081  nqerf  10921  lemul12a  12079  lediv12a  12114  elfzd  13549  fzass4  13597  4fvwrd4  13683  leexp1a  14218  wrd2ind  14767  cshwidxm1  14851  rtrclreclem4  15105  coprmproddvdslem  16726  reumodprminv  16870  prmgaplem6  17122  mreexexlem2d  17707  sgrp2nmndlem4  18996  pmtrrn2  19536  rngcinv  20747  ringcinv  20781  islmodd  20998  nn0srg  21598  rge0srg  21599  mdet1  22769  cpmatmcllem  22886  neitr  23348  restnlly  23650  llyrest  23653  llyidm  23656  uptx  23793  alexsubALTlem2  24216  alexsubALTlem4  24218  distspace  24484  ncvs1  25327  ivthlem3  25623  conway  27983  uzsind  28609  renegscl  28702  readdscl  28703  remulscl  28706  axtg5seg  28745  tglnpt3  28938  colperpexlem3  29024  outpasch  29048  iscgra1  29132  f1otrg  29231  ax5seg  29299  axcontlem4  29328  eengtrkg  29347  wlkonwlk1l  30022  crctcshwlkn0  30181  wwlksnextinj  30259  wwlksnextsurj  30260  clwwlkf1  30411  clwwlknon1  30459  numclwwlk1lem2f1  30719  wlkl0  30729  grpoidinv  30871  pjnmopi  32511  cdj1i  32796  xrofsup  33123  ccfldsrarelvec  34070  dya2iocnrect  34680  omssubadd  34699  sitgfval  34740  bnj969  35343  bnj1463  35452  erdszelem7  35697  rellysconn  35751  segconeq  36510  ifscgr  36544  btwnconn1lem13  36599  btwnconn1lem14  36600  outsideofeq  36630  ellines  36652  fnessref  36896  refssfne  36897  knoppndvlem14  37142  isbasisrelowllem1  38029  isbasisrelowllem2  38030  relowlssretop  38037  itg2gt0cn  38354  frinfm  38414  heiborlem3  38492  isfldidl  38747  eldisjs6  39617  4atlem12  40414  cdleme48fv  41301  cdlemg35  41515  mapd0  42467  aks4d1p1p5  42870  flt4lem7  43419  nna4b4nsq  43420  3cubeslem1  43443  mzpincl  43493  mzpindd  43505  diophin  43531  pellexlem3  43586  pellexlem5  43588  dfno2  44182  amgm3d  44953  amgm4d  44954  lptre2pt  46382  dvnprodlem2  46689  stoweidlem1  46743  stoweidlem14  46756  stoweidlem17  46759  stoweidlem27  46769  stoweidlem57  46799  fourierdlem12  46861  fourierdlem14  46863  fourierdlem70  46918  fourierdlem92  46940  fourierdlem111  46959  etransclem10  46986  etransclem24  47000  salgenval  47063  smfaddlem1  47505  f1cof1blem  47839  elfzelfzlble  48086  reuopreuprim  48303  gpgedgvtx0  48854  rngcinvALTV  49069  ringcinvALTV  49103  lmod1  49300  inlinecirc02plem  49594  nelsubclem  49873  oppf1st2nd  49937