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

Theorem syl9r 78
Description: A nested syllogism inference with different antecedents. (Contributed by NM, 14-May-1993.)
Hypotheses
Ref Expression
syl9r.1 (𝜑 → (𝜓𝜒))
syl9r.2 (𝜃 → (𝜒𝜏))
Assertion
Ref Expression
syl9r (𝜃 → (𝜑 → (𝜓𝜏)))

Proof of Theorem syl9r
StepHypRef Expression
1 syl9r.1 . . 3 (𝜑 → (𝜓𝜒))
2 syl9r.2 . . 3 (𝜃 → (𝜒𝜏))
31, 2syl9 77 . 2 (𝜑 → (𝜃 → (𝜓𝜏)))
43com12 32 1 (𝜃 → (𝜑 → (𝜓𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  sylan9r  693  ax12v2  2198  nfimdOLD  2371  fununi  6125  dfimafn  6408  funimass3  6497  isomin  6751  oneqmin  7171  tz7.48lem  7706  fisupg  8375  fiinfg  8572  trcl  8779  coflim  9295  coftr  9307  axdc3lem2  9485  konigthlem  9602  indpi  9941  nnsub  11271  2ndc1stc  21476  kgencn2  21582  tx1stc  21675  filuni  21910  fclscf  22050  alexsubALTlem2  22073  alexsubALTlem3  22074  alexsubALT  22076  lpni  27664  dfimafnf  29766  dfon2lem6  32019  nodenselem8  32168  finixpnum  33725  heiborlem4  33944  lncvrelatN  35588  imbi13  39246  dfaimafn  41769  sgoldbeven3prm  42199
  Copyright terms: Public domain W3C validator