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

Theorem 3jcad 1133
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 418 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
3 3jcad.2 . . . 4  |-  ( ph  ->  ( ps  ->  th )
)
43imp 418 . . 3  |-  ( (
ph  /\  ps )  ->  th )
5 3jcad.3 . . . 4  |-  ( ph  ->  ( ps  ->  ta ) )
65imp 418 . . 3  |-  ( (
ph  /\  ps )  ->  ta )
72, 4, 63jca 1132 . 2  |-  ( (
ph  /\  ps )  ->  ( ch  /\  th  /\  ta ) )
87ex 423 1  |-  ( ph  ->  ( ps  ->  ( ch  /\  th  /\  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  onfununi  6374  uzm1  10274  ixxssixx  10686  iccid  10717  iccsplit  10784  fzen  10827  fzm1  10878  lmodprop2d  15703  fbun  17551  hausflim  17692  icoopnst  18453  iocopnst  18454  abelth  19833  shsvs  21918  cnlnssadj  22676  cvmlift2lem10  23858  eupai  23898  endofsegid  24780  areacirclem2  25028  elicc3  26331  nbusgra  28277  alrim3con13v  28595  islvol2aN  30403
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator