Theorem jca32 516

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  reuan  3829  sbthlem9  8878  nqerf  10686  lemul12a  11833  lediv12a  11868  elfzd  13247  fzass4  13294  4fvwrd4  13376  leexp1a  13893  wrd2ind  14436  cshwidxm1  14520  rtrclreclem4  14772  coprmproddvdslem  16367  reumodprminv  16505  prmgaplem6  16757  mreexexlem2d  17354  sgrp2nmndlem4  18567  pmtrrn2  19068  islmodd  20129  nn0srg  20668  rge0srg  20669  mdet1  21750  cpmatmcllem  21867  neitr  22331  restnlly  22633  llyrest  22636  llyidm  22639  uptx  22776  alexsubALTlem2  23199  alexsubALTlem4  23201  distspace  23469  ncvs1  24321  ivthlem3  24617  axtg5seg  26826  colperpexlem3  27093  outpasch  27116  iscgra1  27171  f1otrg  27232  ax5seg  27306  axcontlem4  27335  eengtrkg  27354  wlkonwlk1l  28031  crctcshwlkn0  28186  wwlksnextinj  28264  wwlksnextsurj  28265  clwwlkf1  28413  clwwlknon1  28461  numclwwlk1lem2f1  28721  wlkl0  28731  grpoidinv  28870  pjnmopi  30510  cdj1i  30795  xrofsup  31090  ccfldsrarelvec  31741  dya2iocnrect  32248  omssubadd  32267  sitgfval  32308  bnj969  32926  bnj1463  33035  erdszelem7  33159  rellysconn  33213  conway  33993  segconeq  34312  ifscgr  34346  btwnconn1lem13  34401  btwnconn1lem14  34402  outsideofeq  34432  ellines  34454  fnessref  34546  refssfne  34547  knoppndvlem14  34705  isbasisrelowllem1  35526  isbasisrelowllem2  35527  relowlssretop  35534  itg2gt0cn  35832  frinfm  35893  heiborlem3  35971  isfldidl  36226  4atlem12  37626  cdleme48fv  38513  cdlemg35  38727  mapd0  39679  leexp1ad  39980  aks4d1p1p5  40083  flt4lem7  40496  nna4b4nsq  40497  3cubeslem1  40506  mzpincl  40556  mzpindd  40568  diophin  40594  pellexlem3  40653  pellexlem5  40655  amgm3d  41810  amgm4d  41811  lptre2pt  43181  dvnprodlem2  43488  stoweidlem1  43542  stoweidlem14  43555  stoweidlem17  43558  stoweidlem27  43568  stoweidlem57  43598  fourierdlem12  43660  fourierdlem14  43662  fourierdlem70  43717  fourierdlem92  43739  fourierdlem111  43758  etransclem10  43785  etransclem24  43799  salgenval  43862  smfaddlem1  44298  f1cof1blem  44568  elfzelfzlble  44813  reuopreuprim  44978  rngcinv  45539  rngcinvALTV  45551  ringcinv  45590  lmod1  45833  inlinecirc02plem  46132