Theorem sylan9bbr 515

Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)

Hypotheses

Ref	Expression
sylan9bbr.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
sylan9bbr.2	⊢ (𝜃 → (𝜒 ↔ 𝜏))

Assertion

Ref	Expression
sylan9bbr	⊢ ((𝜃 ∧ 𝜑) → (𝜓 ↔ 𝜏))

Proof of Theorem sylan9bbr

Step	Hyp	Ref	Expression
1		sylan9bbr.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		sylan9bbr.2	. . 3 ⊢ (𝜃 → (𝜒 ↔ 𝜏))
3	1, 2	sylan9bb 514	. 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏))
4	3	ancoms 463	1 ⊢ ((𝜃 ∧ 𝜑) → (𝜓 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  bimsc1  842  pm5.75  1027  sbcom2  2166  sbal1  2549  sbal2  2550  sbal2OLD  2551  raaan2  4410  mpteq12f  5108  otthg  5338  fmptsng  6914  f1oiso  7091  mpoeq123  7213  elovmporab  7380  elovmporab1w  7381  elovmporab1  7382  ovmpt3rabdm  7393  elovmpt3rab1  7394  tfindsg  7567  findsg  7602  dfoprab4f  7751  opiota  7754  fmpox  7762  oalimcl  8189  oeeui  8231  nnmword  8262  isinf  8745  elfi  8895  brwdomn0  9051  alephval3  9555  dfac2b  9575  fin17  9839  isfin7-2  9841  ltmpi  10349  addclprlem1  10461  distrlem4pr  10471  1idpr  10474  qreccl  12394  0fz1  12961  zmodid2  13301  ccatrcl1  13980  eqwrds3  14357  divgcdcoprm0  16046  sscntz  18508  gexdvds  18761  cnprest  21974  txrest  22316  ptrescn  22324  flimrest  22668  txflf  22691  fclsrest  22709  tsmssubm  22828  mbfi1fseqlem4  24403  2sq2  26101  axcontlem7  26848  uhgreq12g  26942  nbuhgr2vtx1edgb  27226  wlkcomp  27504  uhgrwkspthlem2  27627  clwlkcomp  27652  wlknwwlksnbij  27758  hashecclwwlkn1  27946  umgrhashecclwwlk  27947  numclwwlk1lem2fo  28227  ubthlem1  28737  pjimai  30043  atcv1  30247  chirredi  30261  bj-restsn  34762  fvineqsneu  35093  pibt2  35099  wl-sbcom2d-lem1  35225  wl-sbalnae  35228  ptrest  35321  poimirlem28  35350  heicant  35357  ftc1anclem1  35395  sbeqi  35862  ralbi12f  35863  iineq12f  35867  brcnvepres  35953  nzss  41379  or2expropbilem1  43975  ich2exprop  44341  ichnreuop  44342  ichreuopeq  44343  reuopreuprim  44396  rngcinv  44957  rngcinvALTV  44969  ringcinv  45008  ringcinvALTV  45032  snlindsntorlem  45229  itscnhlc0xyqsol  45529