Theorem jca32 525

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

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

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 402

This theorem is used by:  reuan  3847  domssl  9008  domssr  9009  sbthlem9  9097  nqerf  10943  lemul12a  12101  lediv12a  12136  elfzd  13573  fzass4  13621  4fvwrd4  13707  leexp1a  14243  wrd2ind  14796  cshwidxm1  14882  rtrclreclem4  15138  coprmproddvdslem  16758  reumodprminv  16902  prmgaplem6  17154  mreexexlem2d  17739  sgrp2nmndlem4  19046  pmtrrn2  19593  rngcinv  20805  ringcinv  20839  islmodd  21056  nn0srg  21656  rge0srg  21657  mdet1  22829  cpmatmcllem  22949  neitr  23411  restnlly  23714  llyrest  23717  llyidm  23720  uptx  23857  alexsubALTlem2  24280  alexsubALTlem4  24282  distspace  24548  ncvs1  25391  ivthlem3  25687  conway  28052  uzsind  28678  renegscl  28771  readdscl  28772  remulscl  28775  axtg5seg  28814  tglnpt3  29009  colperpexlem3  29095  outpasch  29120  iscgra1  29204  f1otrg  29335  ax5seg  29403  axcontlem4  29432  eengtrkg  29451  wlkonwlk1l  30129  crctcshwlkn0  30297  wwlksnextinj  30375  wwlksnextsurj  30376  clwwlkf1  30527  clwwlknon1  30575  numclwwlk1lem2f1  30845  wlkl0  30855  grpoidinv  30997  pjnmopi  32637  cdj1i  32922  xrofsup  33246  ccfldsrarelvec  34189  dya2iocnrect  34800  omssubadd  34819  sitgfval  34860  bnj969  35463  bnj1463  35572  erdszelem7  35784  rellysconn  35838  segconeq  36598  ifscgr  36632  btwnconn1lem13  36687  btwnconn1lem14  36688  outsideofeq  36718  ellines  36740  fnessref  36984  refssfne  36985  knoppndvlem14  37230  isbasisrelowllem1  38117  isbasisrelowllem2  38118  relowlssretop  38125  itg2gt0cn  38432  frinfm  38493  heiborlem3  38571  isfldidl  38826  eldisjs6  39696  4atlem12  40493  cdleme48fv  41380  cdlemg35  41594  mapd0  42546  aks4d1p1p5  42949  flt4lem7  43513  nna4b4nsq  43514  3cubeslem1  43537  mzpincl  43587  mzpindd  43599  diophin  43625  pellexlem3  43680  pellexlem5  43682  dfno2  44276  amgm3d  45047  amgm4d  45048  lptre2pt  46476  dvnprodlem2  46783  stoweidlem1  46837  stoweidlem14  46850  stoweidlem17  46853  stoweidlem27  46863  stoweidlem57  46893  fourierdlem12  46955  fourierdlem14  46957  fourierdlem70  47012  fourierdlem92  47034  fourierdlem111  47053  etransclem10  47080  etransclem24  47094  salgenval  47157  smfaddlem1  47599  f1cof1blem  47970  elfzelfzlble  48217  reuopreuprim  48434  gpgedgvtx0  48985  rngcinvALTV  49199  ringcinvALTV  49233  lmod1  49430  inlinecirc02plem  49724  nelsubclem  50001  oppf1st2nd  50065