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  3633  rextpg  3635  breq12  3992  opelopabg  4251  brabg  4252  opelopab2  4253  ralxpf  4755  rexxpf  4756  feq23  5331  f00  5387  fconstg  5392  f1oeq23  5432  f1o00  5475  f1oiso  5802  riota1a  5825  cbvmpox  5928  caovord  6021  caovord3  6023  rbropapd  6218  genpelvl  7461  genpelvu  7462  nn0ind-raph  9316  elpq  9594  xnn0xadd0  9811  elfz  9958  elfzp12  10042  shftfibg  10771  shftfib  10774  absdvdsb  11758  dvdsabsb  11759  dvdsabseq  11794  tgss2  12832  lmbr  12966  xmetec  13190
  Copyright terms: Public domain W3C validator