Theorem sylan9bbr 510

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 509	. 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏))
4	3	ancoms 458	1 ⊢ ((𝜃 ∧ 𝜑) → (𝜓 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  bimsc1  844  pm5.75  1030  sbcom2  2176  sbal1  2528  sbal2  2529  raaan2  4468  mpteq12f  5174  otthg  5423  dm0rn0  5863  fmptsng  7102  f1oiso  7285  mpoeq123  7418  elovmporab  7592  elovmporab1w  7593  elovmporab1  7594  ovmpt3rabdm  7605  elovmpt3rab1  7606  tfindsg  7791  findsg  7827  dfoprab4f  7988  opiota  7991  fmpox  7999  oalimcl  8475  oeeui  8517  nnmword  8548  isinf  9149  elfi  9297  brwdomn0  9455  alephval3  10001  dfac2b  10022  fin17  10285  isfin7-2  10287  ltmpi  10795  addclprlem1  10907  distrlem4pr  10917  1idpr  10920  qreccl  12867  0fz1  13444  zmodid2  13803  ccatrcl1  14502  eqwrds3  14868  divgcdcoprm0  16576  sscntz  19238  gexdvds  19496  rngcinv  20552  psdmvr  22084  cnprest  23204  txrest  23546  ptrescn  23554  flimrest  23898  txflf  23921  fclsrest  23939  tsmssubm  24058  mbfi1fseqlem4  25646  2sq2  27371  axcontlem7  28948  uhgreq12g  29043  nbuhgr2vtx1edgb  29330  wlkcomp  29609  uhgrwkspthlem2  29732  clwlkcomp  29757  wlknwwlksnbij  29866  hashecclwwlkn1  30057  umgrhashecclwwlk  30058  numclwwlk1lem2fo  30338  ubthlem1  30850  pjimai  32156  atcv1  32360  chirredi  32374  mplvrpmrhm  33577  bj-restsn  37126  fvineqsneu  37455  pibt2  37461  wl-sbcom2d-lem1  37603  wl-sbalnae  37606  ptrest  37658  poimirlem28  37687  heicant  37694  ftc1anclem1  37732  sbeqi  38198  ralbi12f  38199  iineq12f  38203  brcnvepres  38303  elrnressn  38311  tfsconcat0i  43437  nzss  44409  sinnpoly  46990  or2expropbilem1  47131  modmkpkne  47460  ich2exprop  47570  ichnreuop  47571  ichreuopeq  47572  reuopreuprim  47625  rngcinvALTV  48375  snlindsntorlem  48570  itscnhlc0xyqsol  48865  opndisj  49002