Theorem jca32 517

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  reuan  3891  domssl  8994  domssr  8995  sbthlem9  9091  nqerf  10925  lemul12a  12072  lediv12a  12107  elfzd  13492  fzass4  13539  4fvwrd4  13621  leexp1a  14140  wrd2ind  14673  cshwidxm1  14757  rtrclreclem4  15008  coprmproddvdslem  16599  reumodprminv  16737  prmgaplem6  16989  mreexexlem2d  17589  sgrp2nmndlem4  18809  pmtrrn2  19328  islmodd  20477  nn0srg  21015  rge0srg  21016  mdet1  22103  cpmatmcllem  22220  neitr  22684  restnlly  22986  llyrest  22989  llyidm  22992  uptx  23129  alexsubALTlem2  23552  alexsubALTlem4  23554  distspace  23822  ncvs1  24674  ivthlem3  24970  conway  27300  axtg5seg  27716  colperpexlem3  27983  outpasch  28006  iscgra1  28061  f1otrg  28122  ax5seg  28196  axcontlem4  28225  eengtrkg  28244  wlkonwlk1l  28920  crctcshwlkn0  29075  wwlksnextinj  29153  wwlksnextsurj  29154  clwwlkf1  29302  clwwlknon1  29350  numclwwlk1lem2f1  29610  wlkl0  29620  grpoidinv  29761  pjnmopi  31401  cdj1i  31686  xrofsup  31980  ccfldsrarelvec  32745  dya2iocnrect  33280  omssubadd  33299  sitgfval  33340  bnj969  33957  bnj1463  34066  erdszelem7  34188  rellysconn  34242  segconeq  34982  ifscgr  35016  btwnconn1lem13  35071  btwnconn1lem14  35072  outsideofeq  35102  ellines  35124  fnessref  35242  refssfne  35243  knoppndvlem14  35401  isbasisrelowllem1  36236  isbasisrelowllem2  36237  relowlssretop  36244  itg2gt0cn  36543  frinfm  36603  heiborlem3  36681  isfldidl  36936  4atlem12  38483  cdleme48fv  39370  cdlemg35  39584  mapd0  40536  leexp1ad  40837  aks4d1p1p5  40940  flt4lem7  41401  nna4b4nsq  41402  3cubeslem1  41422  mzpincl  41472  mzpindd  41484  diophin  41510  pellexlem3  41569  pellexlem5  41571  dfno2  42179  amgm3d  42951  amgm4d  42952  lptre2pt  44356  dvnprodlem2  44663  stoweidlem1  44717  stoweidlem14  44730  stoweidlem17  44733  stoweidlem27  44743  stoweidlem57  44773  fourierdlem12  44835  fourierdlem14  44837  fourierdlem70  44892  fourierdlem92  44914  fourierdlem111  44933  etransclem10  44960  etransclem24  44974  salgenval  45037  smfaddlem1  45479  f1cof1blem  45784  elfzelfzlble  46029  reuopreuprim  46194  rngcinv  46879  rngcinvALTV  46891  ringcinv  46930  ringcinvALTV  46954  lmod1  47173  inlinecirc02plem  47472