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

Theorem 3jcad 1135
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 419 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
3 3jcad.2 . . . 4  |-  ( ph  ->  ( ps  ->  th )
)
43imp 419 . . 3  |-  ( (
ph  /\  ps )  ->  th )
5 3jcad.3 . . . 4  |-  ( ph  ->  ( ps  ->  ta ) )
65imp 419 . . 3  |-  ( (
ph  /\  ps )  ->  ta )
72, 4, 63jca 1134 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  /\  th  /\  ta ) )
87ex 424 1  |-  ( ph  ->  ( ps  ->  ( ch  /\  th  /\  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  onfununi  6603  uzm1  10516  ixxssixx  10930  iccid  10961  iccsplit  11029  fzen  11072  fzm1  11127  lmodprop2d  16006  fbun  17872  hausflim  18013  icoopnst  18964  iocopnst  18965  abelth  20357  eupai  21689  shsvs  22825  cnlnssadj  23583  cvmlift2lem10  24999  endofsegid  26019  areacirclem1  26292  elicc3  26320  usgra2pth  28311  alrim3con13v  28617  islvol2aN  30389
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator