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

Theorem sylan9bb 438
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  439  bi2anan9  526  syl3an9b  1188  sbcomxyyz  1824  eqeq12  2030  eleq12  2080  sbhypf  2576  ceqsrex2v  2649  sseq12  2941  rexprg  3392  rextpg  3394  breq12  3739  opelopabg  3975  brabg  3976  opelopab2  3977  ralxpf  4405  rexxpf  4406  feq23  4955  f00  5002  fconstg  5004  f1oeq23  5041  f1o00  5082  f1oiso  5386  riota1a  5407  cbvmpt2x  5501  caovord  5591  caovord3  5593  genpelvl  6360  genpelvu  6361
  Copyright terms: Public domain W3C validator