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

Theorem sylan9bb 450
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 270 . 2 ((𝜑𝜃) → (𝜓𝜒))
3 sylan9bb.2 . . 3 (𝜃 → (𝜒𝜏))
43adantl 271 . 2 ((𝜑𝜃) → (𝜒𝜏))
52, 4bitrd 186 1 ((𝜑𝜃) → (𝜓𝜏))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  sylan9bbr  451  bi2anan9  571  baibd  868  rbaibd  869  syl3an9b  1244  sbcomxyyz  1891  eqeq12  2097  eleq12  2149  sbhypf  2662  ceqsrex2v  2740  sseq12  3038  rexprg  3477  rextpg  3479  breq12  3825  opelopabg  4069  brabg  4070  opelopab2  4071  ralxpf  4550  rexxpf  4551  feq23  5113  f00  5165  fconstg  5170  f1oeq23  5210  f1o00  5251  f1oiso  5566  riota1a  5588  cbvmpt2x  5683  caovord  5773  caovord3  5775  genpelvl  7015  genpelvu  7016  nn0ind-raph  8796  elfz  9362  elfzp12  9443  shftfibg  10150  shftfib  10153  absdvdsb  10689  dvdsabsb  10690  dvdsabseq  10723
  Copyright terms: Public domain W3C validator