New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  sylan9bb GIF version

Theorem sylan9bb 680
 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 451 . 2 ((φ θ) → (ψχ))
3 sylan9bb.2 . . 3 (θ → (χτ))
43adantl 452 . 2 ((φ θ) → (χτ))
52, 4bitrd 244 1 ((φ θ) → (ψτ))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 177  df-an 360 This theorem is referenced by:  sylan9bbr  681  bi2anan9  843  baibd  875  rbaibd  876  syl3an9b  1250  nanbi12  1297  sbcom  2089  sbcom2  2114  ax11eq  2193  ax11el  2194  eqeq12  2365  eleq12  2415  sbhypf  2904  ceqsrex2v  2974  sseq12  3294  rexprg  3776  rextpg  3778  otkelins2kg  4253  otkelins3kg  4254  opkelcokg  4261  sfintfin  4532  breq12  4644  opelopabg  4705  brabg  4706  opelopab2  4707  ralxpf  4827  feq23  5213  f00  5249  fconstg  5251  f1oeq23  5284  f1o00  5317  f1oiso  5499  caovord  5629  caovord3  5631  cbvmpt2x  5678  ovmpt2x  5712  composefn  5818  fnfullfun  5858  elce  6175  ce2  6192
 Copyright terms: Public domain W3C validator