Theorem jca32 518

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  reuan  3873  sbthlem9  8628  nqerf  10345  lemul12a  11491  lediv12a  11526  fzass4  12942  4fvwrd4  13024  leexp1a  13536  wrd2ind  14080  cshwidxm1  14164  rtrclreclem4  14415  coprmproddvdslem  16001  reumodprminv  16136  prmgaplem6  16387  mreexexlem2d  16911  sgrp2nmndlem4  18088  pmtrrn2  18583  islmodd  19635  nn0srg  20610  rge0srg  20611  mdet1  21205  cpmatmcllem  21321  neitr  21783  restnlly  22085  llyrest  22088  llyidm  22091  uptx  22228  alexsubALTlem2  22651  alexsubALTlem4  22653  distspace  22921  ncvs1  23756  ivthlem3  24049  axtg5seg  26249  colperpexlem3  26516  outpasch  26539  iscgra1  26594  f1otrg  26655  ax5seg  26722  axcontlem4  26751  eengtrkg  26770  wlkonwlk1l  27443  crctcshwlkn0  27597  wwlksnextinj  27675  wwlksnextsurj  27676  clwwlkf1  27826  clwwlknon1  27874  numclwwlk1lem2f1  28134  wlkl0  28144  grpoidinv  28283  pjnmopi  29923  cdj1i  30208  xrofsup  30492  ccfldsrarelvec  31080  dya2iocnrect  31560  omssubadd  31579  sitgfval  31620  bnj969  32239  bnj1463  32348  erdszelem7  32465  rellysconn  32519  conway  33285  etasslt  33295  segconeq  33492  ifscgr  33526  btwnconn1lem13  33581  btwnconn1lem14  33582  outsideofeq  33612  ellines  33634  fnessref  33726  refssfne  33727  knoppndvlem14  33885  isbasisrelowllem1  34660  isbasisrelowllem2  34661  relowlssretop  34668  itg2gt0cn  34982  frinfm  35043  heiborlem3  35124  isfldidl  35379  4atlem12  36781  cdleme48fv  37668  cdlemg35  37882  mapd0  38834  3cubeslem1  39357  mzpincl  39407  mzpindd  39419  diophin  39445  pellexlem3  39504  pellexlem5  39506  amgm3d  40626  amgm4d  40627  monoords  41638  uzfissfz  41668  iuneqfzuzlem  41676  ssuzfz  41691  elfzd  41757  mccllem  41952  sumnnodd  41985  lptre2pt  41995  dvnmul  42302  dvnprodlem1  42305  dvnprodlem2  42306  itgspltprt  42338  stoweidlem1  42360  stoweidlem3  42362  stoweidlem14  42373  stoweidlem17  42376  stoweidlem27  42386  stoweidlem57  42416  fourierdlem12  42478  fourierdlem14  42480  fourierdlem41  42507  fourierdlem48  42513  fourierdlem49  42514  fourierdlem50  42515  fourierdlem70  42535  fourierdlem79  42544  fourierdlem92  42557  fourierdlem111  42576  elaa2lem  42592  etransclem3  42596  etransclem7  42600  etransclem10  42603  etransclem24  42617  etransclem27  42620  etransclem28  42621  etransclem35  42628  etransclem38  42631  etransclem44  42637  salgenval  42680  iundjiun  42816  caratheodorylem1  42882  smfaddlem1  43113  elfzelfzlble  43595  reuopreuprim  43762  rngcinv  44326  rngcinvALTV  44338  ringcinv  44377  lmod1  44621  inlinecirc02plem  44847