MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3jcad Structured version   Unicode version

Theorem 3jcad 1177
Description: Deduction conjoining the consequents of three implications. (Contributed by NM, 25-Sep-2005.)
Hypotheses
Ref Expression
3jcad.1  |-  ( ph  ->  ( ps  ->  ch ) )
3jcad.2  |-  ( ph  ->  ( ps  ->  th )
)
3jcad.3  |-  ( ph  ->  ( ps  ->  ta ) )
Assertion
Ref Expression
3jcad  |-  ( ph  ->  ( ps  ->  ( ch  /\  th  /\  ta ) ) )

Proof of Theorem 3jcad
StepHypRef Expression
1 3jcad.1 . . . 4  |-  ( ph  ->  ( ps  ->  ch ) )
21imp 429 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
3 3jcad.2 . . . 4  |-  ( ph  ->  ( ps  ->  th )
)
43imp 429 . . 3  |-  ( (
ph  /\  ps )  ->  th )
5 3jcad.3 . . . 4  |-  ( ph  ->  ( ps  ->  ta ) )
65imp 429 . . 3  |-  ( (
ph  /\  ps )  ->  ta )
72, 4, 63jca 1176 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  /\  th  /\  ta ) )
87ex 434 1  |-  ( ph  ->  ( ps  ->  ( ch  /\  th  /\  ta ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 185  df-an 371  df-3an 975
This theorem is referenced by:  onfununi  7012  uzm1  11112  ixxssixx  11543  iccid  11574  iccsplit  11653  fzen  11703  fzm1  11758  lmodprop2d  17372  fbun  20104  hausflim  20245  icoopnst  21202  iocopnst  21203  abelth  22598  eupai  24671  shsvs  25945  cnlnssadj  26703  cvmlift2lem10  28425  endofsegid  29340  areacirclem1  29712  elicc3  29740  usgra2pth  31849  alrim3con13v  32401  islvol2aN  34406
  Copyright terms: Public domain W3C validator