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 406 . . 3 ((𝜑𝜓) → 𝜒)
3 3jcad.2 . . . 4 (𝜑 → (𝜓𝜃))
43imp 406 . . 3 ((𝜑𝜓) → 𝜃)
5 3jcad.3 . . . 4 (𝜑 → (𝜓𝜏))
65imp 406 . . 3 ((𝜑𝜓) → 𝜏)
72, 4, 63jca 1128 . 2 ((𝜑𝜓) → (𝜒𝜃𝜏))
87ex 412 1 (𝜑 → (𝜓 → (𝜒𝜃𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1086
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 207  df-an 396  df-3an 1088
This theorem is referenced by:  onfununi  8382  uzm1  12917  ixxssixx  13402  iccid  13433  iccsplit  13526  fzen  13582  lmodprop2d  20923  fbun  23849  hausflim  23990  icoopnst  24970  iocopnst  24971  abelth  26486  usgr2pth  29785  shsvs  31343  cnlnssadj  32100  fnrelpredd  35104  cvmlift2lem10  35318  endofsegid  36087  elicc3  36319  areacirclem1  37716  islvol2aN  39595  alrim3con13v  44558  ormkglobd  46895  bgoldbtbndlem4  47800
  Copyright terms: Public domain W3C validator