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

Theorem 3jcad 1380
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 444 . . 3 ((𝜑𝜓) → 𝜒)
3 3jcad.2 . . . 4 (𝜑 → (𝜓𝜃))
43imp 444 . . 3 ((𝜑𝜓) → 𝜃)
5 3jcad.3 . . . 4 (𝜑 → (𝜓𝜏))
65imp 444 . . 3 ((𝜑𝜓) → 𝜏)
72, 4, 63jca 1379 . 2 ((𝜑𝜓) → (𝜒𝜃𝜏))
87ex 449 1 (𝜑 → (𝜓 → (𝜒𝜃𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 197  df-an 385  df-3an 1074
This theorem is referenced by:  onfununi  7558  uzm1  11832  ixxssixx  12303  iccid  12334  iccsplit  12419  fzen  12472  lmodprop2d  19048  fbun  21766  hausflim  21907  icoopnst  22860  iocopnst  22861  abelth  24315  usgr2pth  26791  shsvs  28412  cnlnssadj  29169  cvmlift2lem10  31522  endofsegid  32419  elicc3  32538  areacirclem1  33732  islvol2aN  35298  alrim3con13v  39162  bgoldbtbndlem4  42123
  Copyright terms: Public domain W3C validator