ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sylan9bb GIF version

Theorem sylan9bb 459
Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)
Hypotheses
Ref Expression
sylan9bb.1 (𝜑 → (𝜓𝜒))
sylan9bb.2 (𝜃 → (𝜒𝜏))
Assertion
Ref Expression
sylan9bb ((𝜑𝜃) → (𝜓𝜏))

Proof of Theorem sylan9bb
StepHypRef Expression
1 sylan9bb.1 . . 3 (𝜑 → (𝜓𝜒))
21adantr 274 . 2 ((𝜑𝜃) → (𝜓𝜒))
3 sylan9bb.2 . . 3 (𝜃 → (𝜒𝜏))
43adantl 275 . 2 ((𝜑𝜃) → (𝜒𝜏))
52, 4bitrd 187 1 ((𝜑𝜃) → (𝜓𝜏))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  sylan9bbr  460  bi2anan9  601  baibd  918  rbaibd  919  syl3an9b  1305  sbcomxyyz  1965  eqeq12  2183  eleq12  2235  sbhypf  2779  ceqsrex2v  2862  sseq12  3172  rexprg  3635  rextpg  3637  breq12  3994  opelopabg  4253  brabg  4254  opelopab2  4255  ralxpf  4757  rexxpf  4758  feq23  5333  f00  5389  fconstg  5394  f1oeq23  5434  f1o00  5477  f1oiso  5805  riota1a  5828  cbvmpox  5931  caovord  6024  caovord3  6026  rbropapd  6221  genpelvl  7474  genpelvu  7475  nn0ind-raph  9329  elpq  9607  xnn0xadd0  9824  elfz  9971  elfzp12  10055  shftfibg  10784  shftfib  10787  absdvdsb  11771  dvdsabsb  11772  dvdsabseq  11807  tgss2  12873  lmbr  13007  xmetec  13231
  Copyright terms: Public domain W3C validator