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

Theorem 3jcad 1136
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 420 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
3 3jcad.2 . . . 4  |-  ( ph  ->  ( ps  ->  th )
)
43imp 420 . . 3  |-  ( (
ph  /\  ps )  ->  th )
5 3jcad.3 . . . 4  |-  ( ph  ->  ( ps  ->  ta ) )
65imp 420 . . 3  |-  ( (
ph  /\  ps )  ->  ta )
72, 4, 63jca 1135 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  /\  th  /\  ta ) )
87ex 425 1  |-  ( ph  ->  ( ps  ->  ( ch  /\  th  /\  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  onfununi  6605  uzm1  10518  ixxssixx  10932  iccid  10963  iccsplit  11031  fzen  11074  fzm1  11129  lmodprop2d  16008  fbun  17874  hausflim  18015  icoopnst  18966  iocopnst  18967  abelth  20359  eupai  21691  shsvs  22827  cnlnssadj  23585  cvmlift2lem10  25001  endofsegid  26021  areacirclem1  26294  elicc3  26322  usgra2pth  28337  alrim3con13v  28679  islvol2aN  30451
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator