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

Theorem 3jcad 1169
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 1168 . 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 965
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 967
This theorem is referenced by:  onfununi  6807  uzm1  10896  ixxssixx  11319  iccid  11350  iccsplit  11423  fzen  11472  fzm1  11545  lmodprop2d  17012  fbun  19418  hausflim  19559  icoopnst  20516  iocopnst  20517  abelth  21911  eupai  23593  shsvs  24731  cnlnssadj  25489  cvmlift2lem10  27206  endofsegid  28121  areacirclem1  28489  elicc3  28517  usgra2pth  30306  alrim3con13v  31244  islvol2aN  33241
  Copyright terms: Public domain W3C validator