Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  jca31 Structured version   Visualization version   GIF version

Theorem jca31 556
 Description: Join three consequents. (Contributed by Jeff Hankins, 1-Aug-2009.)
Hypotheses
Ref Expression
jca31.1 (𝜑𝜓)
jca31.2 (𝜑𝜒)
jca31.3 (𝜑𝜃)
Assertion
Ref Expression
jca31 (𝜑 → ((𝜓𝜒) ∧ 𝜃))

Proof of Theorem jca31
StepHypRef Expression
1 jca31.1 . . 3 (𝜑𝜓)
2 jca31.2 . . 3 (𝜑𝜒)
31, 2jca 554 . 2 (𝜑 → (𝜓𝜒))
4 jca31.3 . 2 (𝜑𝜃)
53, 4jca 554 1 (𝜑 → ((𝜓𝜒) ∧ 𝜃))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384 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 197  df-an 386 This theorem is referenced by:  3jca  1240  syl21anc  1322  xpdifid  5523  tpres  6423  f1oiso2  6559  oewordri  7620  boxriin  7897  cantnfrescl  8520  cfsuc  9026  genpcl  9777  ltexprlem5  9809  prsrlem1  9840  lemulge11  10832  lediv12a  10863  elnnz  11334  quoremz  12597  quoremnn0ALT  12599  fldiv  12602  modsumfzodifsn  12686  leexp1a  12862  faclbnd6  13029  wrdlen2i  13623  wwlktovfo  13638  setcinv  16664  sgrp2rid2  17337  grpidinv2  17398  mhmfmhm  17462  gsumval3lem1  18230  dvdsrzring  19753  scmatmhm  20262  cncnp2  20998  vitalilem1  23289  vitalilem1OLD  23290  aaliou3lem2  24009  pntibndlem2  25187  iscgrglt  25316  islnoppd  25539  oppcom  25543  opphllem1  25546  opphllem2  25547  opphllem5  25550  oppperpex  25552  hpgerlem  25564  colopp  25568  colhp  25569  ax5seg  25725  uhgr2edg  26000  nbupgrres  26160  usgr2pthlem  26535  crctcshwlkn0lem5  26582  wlknwwlksnsur  26652  wlkwwlksur  26659  1pthond  26877  3pthdlem1  26897  frgrncvvdeqlem4  27037  fusgr2wsp2nb  27063  grpoidinv  27223  nmcvcn  27411  leopmul  28854  resf1o  29360  rhmopp  29616  oddpwdc  30209  poseq  31472  btwnconn1  31871  finminlem  31975  bj-elid3  32741  ptrecube  33062  poimirlem22  33084  isrngod  33350  paddasslem4  34610  cdleme21h  35123  cdleme26eALTN  35150  cdleme40m  35256  cdlemf2  35351  dicssdvh  35976  dihopelvalcpre  36038  dihmeetlem4preN  36096  dih1dimatlem0  36118  lzenom  36834  jm2.27c  37075  clrellem  37431  2pm13.193  38271  disjxp1  38742  dmrelrnrel  38911  infleinflem2  39069  mullimc  39270  mullimcf  39277  addlimc  39302  0ellimcdiv  39303  cncfshift  39408  cncfperiod  39413  icccncfext  39421  stoweidlem52  39592  wallispilem4  39608  fourierdlem16  39663  fourierdlem21  39668  fourierdlem48  39694  fourierdlem51  39697  fourierdlem52  39698  fourierdlem54  39700  fourierdlem64  39710  fourierdlem76  39722  fourierdlem77  39723  fourierdlem80  39726  fourierdlem86  39732  fourierdlem87  39733  fourierdlem102  39748  fourierdlem114  39760  sge0f1o  39922  sge0split  39949  ismea  39991  nnfoctbdjlem  39995  iundjiun  40000  ismeannd  40007  psmeasure  40011  isomennd  40068  hoidmvle  40137  ovncvr2  40148  oexpnegnz  40904  rngcinv  41285  rngcinvALTV  41297  ringcinv  41336  ringcinvALTV  41360
 Copyright terms: Public domain W3C validator