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

Theorem sylan9bb 457
 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  458  bi2anan9  595  baibd  908  rbaibd  909  syl3an9b  1288  sbcomxyyz  1945  eqeq12  2152  eleq12  2204  sbhypf  2735  ceqsrex2v  2817  sseq12  3122  rexprg  3575  rextpg  3577  breq12  3934  opelopabg  4190  brabg  4191  opelopab2  4192  ralxpf  4685  rexxpf  4686  feq23  5258  f00  5314  fconstg  5319  f1oeq23  5359  f1o00  5402  f1oiso  5727  riota1a  5749  cbvmpox  5849  caovord  5942  caovord3  5944  rbropapd  6139  genpelvl  7327  genpelvu  7328  nn0ind-raph  9175  xnn0xadd0  9657  elfz  9803  elfzp12  9886  shftfibg  10599  shftfib  10602  absdvdsb  11517  dvdsabsb  11518  dvdsabseq  11551  tgss2  12257  lmbr  12391  xmetec  12615
 Copyright terms: Public domain W3C validator