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

Theorem sylan9bb 443
 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 265 . 2 ((𝜑𝜃) → (𝜓𝜒))
3 sylan9bb.2 . . 3 (𝜃 → (𝜒𝜏))
43adantl 266 . 2 ((𝜑𝜃) → (𝜒𝜏))
52, 4bitrd 181 1 ((𝜑𝜃) → (𝜓𝜏))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   ↔ wb 102 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  sylan9bbr  444  bi2anan9  548  baibd  843  rbaibd  844  syl3an9b  1216  sbcomxyyz  1862  eqeq12  2068  eleq12  2118  sbhypf  2620  ceqsrex2v  2699  sseq12  2996  rexprg  3450  rextpg  3452  breq12  3797  opelopabg  4033  brabg  4034  opelopab2  4035  ralxpf  4510  rexxpf  4511  feq23  5061  f00  5109  fconstg  5111  f1oeq23  5148  f1o00  5189  f1oiso  5493  riota1a  5515  cbvmpt2x  5610  caovord  5700  caovord3  5702  genpelvl  6668  genpelvu  6669  nn0ind-raph  8414  elfz  8982  elfzp12  9063  shftfibg  9649  shftfib  9652  absdvdsb  10126  dvdsabsb  10127  dvdsabseq  10159
 Copyright terms: Public domain W3C validator