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

Theorem 3jcad 1123
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 407 . . 3 ((𝜑𝜓) → 𝜒)
3 3jcad.2 . . . 4 (𝜑 → (𝜓𝜃))
43imp 407 . . 3 ((𝜑𝜓) → 𝜃)
5 3jcad.3 . . . 4 (𝜑 → (𝜓𝜏))
65imp 407 . . 3 ((𝜑𝜓) → 𝜏)
72, 4, 63jca 1122 . 2 ((𝜑𝜓) → (𝜒𝜃𝜏))
87ex 413 1 (𝜑 → (𝜓 → (𝜒𝜃𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1081
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 208  df-an 397  df-3an 1083
This theorem is referenced by:  onfununi  7969  uzm1  12265  ixxssixx  12742  iccid  12773  iccsplit  12861  fzen  12914  lmodprop2d  19616  fbun  22364  hausflim  22505  icoopnst  23458  iocopnst  23459  abelth  24944  usgr2pth  27459  shsvs  29014  cnlnssadj  29771  cvmlift2lem10  32443  endofsegid  33430  elicc3  33549  areacirclem1  34849  islvol2aN  36595  alrim3con13v  40732  bgoldbtbndlem4  43805
  Copyright terms: Public domain W3C validator