Theorem jca32 519

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  reuan  3795  sbthlem9  8742  nqerf  10509  lemul12a  11655  lediv12a  11690  elfzd  13068  fzass4  13115  4fvwrd4  13197  leexp1a  13710  wrd2ind  14253  cshwidxm1  14337  rtrclreclem4  14589  coprmproddvdslem  16182  reumodprminv  16320  prmgaplem6  16572  mreexexlem2d  17102  sgrp2nmndlem4  18309  pmtrrn2  18806  islmodd  19859  nn0srg  20387  rge0srg  20388  mdet1  21452  cpmatmcllem  21569  neitr  22031  restnlly  22333  llyrest  22336  llyidm  22339  uptx  22476  alexsubALTlem2  22899  alexsubALTlem4  22901  distspace  23168  ncvs1  24008  ivthlem3  24304  axtg5seg  26510  colperpexlem3  26777  outpasch  26800  iscgra1  26855  f1otrg  26916  ax5seg  26983  axcontlem4  27012  eengtrkg  27031  wlkonwlk1l  27705  crctcshwlkn0  27859  wwlksnextinj  27937  wwlksnextsurj  27938  clwwlkf1  28086  clwwlknon1  28134  numclwwlk1lem2f1  28394  wlkl0  28404  grpoidinv  28543  pjnmopi  30183  cdj1i  30468  xrofsup  30764  ccfldsrarelvec  31409  dya2iocnrect  31914  omssubadd  31933  sitgfval  31974  bnj969  32593  bnj1463  32702  erdszelem7  32826  rellysconn  32880  conway  33679  segconeq  33998  ifscgr  34032  btwnconn1lem13  34087  btwnconn1lem14  34088  outsideofeq  34118  ellines  34140  fnessref  34232  refssfne  34233  knoppndvlem14  34391  isbasisrelowllem1  35212  isbasisrelowllem2  35213  relowlssretop  35220  itg2gt0cn  35518  frinfm  35579  heiborlem3  35657  isfldidl  35912  4atlem12  37312  cdleme48fv  38199  cdlemg35  38413  mapd0  39365  leexp1ad  39662  aks4d1p1p5  39765  nna4b4nsq  40141  3cubeslem1  40150  mzpincl  40200  mzpindd  40212  diophin  40238  pellexlem3  40297  pellexlem5  40299  amgm3d  41429  amgm4d  41430  lptre2pt  42799  dvnprodlem2  43106  stoweidlem1  43160  stoweidlem14  43173  stoweidlem17  43176  stoweidlem27  43186  stoweidlem57  43216  fourierdlem12  43278  fourierdlem14  43280  fourierdlem70  43335  fourierdlem92  43357  fourierdlem111  43376  etransclem10  43403  etransclem24  43417  salgenval  43480  smfaddlem1  43913  f1cof1blem  44183  elfzelfzlble  44429  reuopreuprim  44594  rngcinv  45155  rngcinvALTV  45167  ringcinv  45206  lmod1  45449  inlinecirc02plem  45748