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

Theorem 3jcad 1129
Description: Deduction conjoining the consequents of three implications. (Contributed by NM, 25-Sep-2005.)
Hypotheses
Ref Expression
3jcad.1 (𝜑 → (𝜓𝜒))
3jcad.2 (𝜑 → (𝜓𝜃))
3jcad.3 (𝜑 → (𝜓𝜏))
Assertion
Ref Expression
3jcad (𝜑 → (𝜓 → (𝜒𝜃𝜏)))

Proof of Theorem 3jcad
StepHypRef Expression
1 3jcad.1 . . . 4 (𝜑 → (𝜓𝜒))
21imp 407 . . 3 ((𝜑𝜓) → 𝜒)
3 3jcad.2 . . . 4 (𝜑 → (𝜓𝜃))
43imp 407 . . 3 ((𝜑𝜓) → 𝜃)
5 3jcad.3 . . . 4 (𝜑 → (𝜓𝜏))
65imp 407 . . 3 ((𝜑𝜓) → 𝜏)
72, 4, 63jca 1128 . 2 ((𝜑𝜓) → (𝜒𝜃𝜏))
87ex 413 1 (𝜑 → (𝜓 → (𝜒𝜃𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1087
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 206  df-an 397  df-3an 1089
This theorem is referenced by:  onfununi  8340  uzm1  12859  ixxssixx  13337  iccid  13368  iccsplit  13461  fzen  13517  lmodprop2d  20533  fbun  23343  hausflim  23484  icoopnst  24454  iocopnst  24455  abelth  25952  usgr2pth  29018  shsvs  30571  cnlnssadj  31328  fnrelpredd  34087  cvmlift2lem10  34298  endofsegid  35052  elicc3  35197  areacirclem1  36571  islvol2aN  38458  alrim3con13v  43284  bgoldbtbndlem4  46466
  Copyright terms: Public domain W3C validator