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  3844  domssl  9009  domssr  9010  sbthlem9  9098  nqerf  10996  lemul12a  12156  lediv12a  12191  elfzd  13628  fzass4  13676  4fvwrd4  13762  leexp1a  14298  wrd2ind  14852  cshwidxm1  14938  rtrclreclem4  15194  coprmproddvdslem  16817  reumodprminv  16962  prmgaplem6  17214  mreexexlem2d  17799  sgrp2nmndlem4  19107  pmtrrn2  19654  rngcinv  20869  ringcinv  20903  islmodd  21121  nn0srg  21723  rge0srg  21724  mdet1  22896  cpmatmcllem  23016  neitr  23478  restnlly  23781  llyrest  23784  llyidm  23787  uptx  23924  alexsubALTlem2  24347  alexsubALTlem4  24349  distspace  24615  ncvs1  25458  ivthlem3  25754  flt4lem7  27971  nna4b4nsq  27972  conway  28147  uzsind  28773  renegscl  28866  readdscl  28867  remulscl  28870  axtg5seg  28909  tglnpt3  29104  colperpexlem3  29190  outpasch  29215  iscgra1  29299  f1otrg  29430  ax5seg  29498  axcontlem4  29527  eengtrkg  29546  wlkonwlk1l  30224  crctcshwlkn0  30392  wwlksnextinj  30470  wwlksnextsurj  30471  clwwlkf1  30622  clwwlknon1  30670  numclwwlk1lem2f1  30940  wlkl0  30950  grpoidinv  31092  pjnmopi  32732  cdj1i  33017  xrofsup  33341  ccfldsrarelvec  34285  dya2iocnrect  34896  omssubadd  34915  sitgfval  34956  bnj969  35559  bnj1463  35668  erdszelem7  35931  rellysconn  35985  segconeq  36745  ifscgr  36779  btwnconn1lem13  36834  btwnconn1lem14  36835  outsideofeq  36865  ellines  36887  fnessref  37115  refssfne  37116  knoppndvlem14  37361  isbasisrelowllem1  38246  isbasisrelowllem2  38247  relowlssretop  38254  itg2gt0cn  38561  frinfm  38637  heiborlem3  38715  isfldidl  38970  eldisjs6  39840  4atlem12  40637  cdleme48fv  41524  cdlemg35  41738  mapd0  42690  aks4d1p1p5  43093  3cubeslem1  43648  mzpincl  43698  mzpindd  43710  diophin  43736  pellexlem3  43791  pellexlem5  43793  dfno2  44387  amgm3d  45158  amgm4d  45159  lptre2pt  46594  dvnprodlem2  46901  stoweidlem1  46955  stoweidlem14  46968  stoweidlem17  46971  stoweidlem27  46981  stoweidlem57  47011  fourierdlem12  47073  fourierdlem14  47075  fourierdlem70  47130  fourierdlem92  47152  fourierdlem111  47171  etransclem10  47198  etransclem24  47212  salgenval  47275  smfaddlem1  47717  f1cof1blem  48088  elfzelfzlble  48335  reuopreuprim  48552  gpgedgvtx0  49103  rngcinvALTV  49317  ringcinvALTV  49351  lmod1  49548  inlinecirc02plem  49842  nelsubclem  50119  oppf1st2nd  50183