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

Theorem sylan9bb 451
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 271 . 2 ((𝜑𝜃) → (𝜓𝜒))
3 sylan9bb.2 . . 3 (𝜃 → (𝜒𝜏))
43adantl 272 . 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-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  sylan9bbr  452  bi2anan9  574  baibd  873  rbaibd  874  syl3an9b  1253  sbcomxyyz  1901  eqeq12  2107  eleq12  2159  sbhypf  2682  ceqsrex2v  2763  sseq12  3064  rexprg  3514  rextpg  3516  breq12  3872  opelopabg  4119  brabg  4120  opelopab2  4121  ralxpf  4613  rexxpf  4614  feq23  5182  f00  5237  fconstg  5242  f1oeq23  5282  f1o00  5323  f1oiso  5643  riota1a  5665  cbvmpt2x  5764  caovord  5854  caovord3  5856  genpelvl  7168  genpelvu  7169  nn0ind-raph  8962  xnn0xadd0  9433  elfz  9579  elfzp12  9662  shftfibg  10385  shftfib  10388  absdvdsb  11257  dvdsabsb  11258  dvdsabseq  11291  tgss2  11947  lmbr  12080  xmetec  12239
  Copyright terms: Public domain W3C validator