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

Theorem sylan9bb 435
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 261 . 2 ((φ θ) → (ψχ))
3 sylan9bb.2 . . 3 (θ → (χτ))
43adantl 262 . 2 ((φ θ) → (χτ))
52, 4bitrd 177 1 ((φ θ) → (ψτ))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  sylan9bbr  436  bi2anan9  538  baibd  831  rbaibd  832  syl3an9b  1204  sbcomxyyz  1843  eqeq12  2049  eleq12  2099  sbhypf  2597  ceqsrex2v  2670  sseq12  2962  rexprg  3413  rextpg  3415  breq12  3760  opelopabg  3996  brabg  3997  opelopab2  3998  ralxpf  4425  rexxpf  4426  feq23  4976  f00  5024  fconstg  5026  f1oeq23  5063  f1o00  5104  f1oiso  5408  riota1a  5430  cbvmpt2x  5524  caovord  5614  caovord3  5616  genpelvl  6494  genpelvu  6495  nn0ind-raph  8111  elfz  8630  elfzp12  8711
  Copyright terms: Public domain W3C validator