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

Theorem 3jcad 1152
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 395 . . 3 ((𝜑𝜓) → 𝜒)
3 3jcad.2 . . . 4 (𝜑 → (𝜓𝜃))
43imp 395 . . 3 ((𝜑𝜓) → 𝜃)
5 3jcad.3 . . . 4 (𝜑 → (𝜓𝜏))
65imp 395 . . 3 ((𝜑𝜓) → 𝜏)
72, 4, 63jca 1151 . 2 ((𝜑𝜓) → (𝜒𝜃𝜏))
87ex 399 1 (𝜑 → (𝜓 → (𝜒𝜃𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  onfununi  7677  uzm1  11939  ixxssixx  12410  iccid  12441  iccsplit  12531  fzen  12584  lmodprop2d  19132  fbun  21861  hausflim  22002  icoopnst  22955  iocopnst  22956  abelth  24415  usgr2pth  26894  shsvs  28516  cnlnssadj  29273  cvmlift2lem10  31622  endofsegid  32518  elicc3  32637  areacirclem1  33814  islvol2aN  35374  alrim3con13v  39242  bgoldbtbndlem4  42272
  Copyright terms: Public domain W3C validator