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  8291  uzm1  12809  ixxssixx  13287  iccid  13318  iccsplit  13411  fzen  13467  lmodprop2d  20428  fbun  23214  hausflim  23355  icoopnst  24325  iocopnst  24326  abelth  25823  usgr2pth  28761  shsvs  30314  cnlnssadj  31071  fnrelpredd  33757  cvmlift2lem10  33970  endofsegid  34723  elicc3  34842  areacirclem1  36216  islvol2aN  38105  alrim3con13v  42907  bgoldbtbndlem4  46090
  Copyright terms: Public domain W3C validator