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

Theorem 3jcad 1130
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 408 . . 3 ((𝜑𝜓) → 𝜒)
3 3jcad.2 . . . 4 (𝜑 → (𝜓𝜃))
43imp 408 . . 3 ((𝜑𝜓) → 𝜃)
5 3jcad.3 . . . 4 (𝜑 → (𝜓𝜏))
65imp 408 . . 3 ((𝜑𝜓) → 𝜏)
72, 4, 63jca 1129 . 2 ((𝜑𝜓) → (𝜒𝜃𝜏))
87ex 414 1 (𝜑 → (𝜓 → (𝜒𝜃𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 398  df-3an 1090
This theorem is referenced by:  onfununi  8341  uzm1  12860  ixxssixx  13338  iccid  13369  iccsplit  13462  fzen  13518  lmodprop2d  20534  fbun  23344  hausflim  23485  icoopnst  24455  iocopnst  24456  abelth  25953  usgr2pth  29021  shsvs  30576  cnlnssadj  31333  fnrelpredd  34092  cvmlift2lem10  34303  endofsegid  35057  elicc3  35202  areacirclem1  36576  islvol2aN  38463  alrim3con13v  43294  bgoldbtbndlem4  46476
  Copyright terms: Public domain W3C validator