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

Theorem 3jcad 1128
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 1127 . 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  8380  uzm1  12914  ixxssixx  13398  iccid  13429  iccsplit  13522  fzen  13578  lmodprop2d  20939  fbun  23864  hausflim  24005  icoopnst  24983  iocopnst  24984  abelth  26500  usgr2pth  29797  shsvs  31352  cnlnssadj  32109  fnrelpredd  35082  cvmlift2lem10  35297  endofsegid  36067  elicc3  36300  areacirclem1  37695  islvol2aN  39575  alrim3con13v  44531  bgoldbtbndlem4  47733
  Copyright terms: Public domain W3C validator