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  845  pm5.75  1031  sbcom2  2179  sbal1  2532  sbal2  2533  raaan2  4462  mpteq12f  5170  otthg  5438  dm0rn0  5879  fmptsng  7123  f1oiso  7306  mpoeq123  7439  elovmporab  7613  elovmporab1w  7614  elovmporab1  7615  ovmpt3rabdm  7626  elovmpt3rab1  7627  tfindsg  7812  findsg  7848  dfoprab4f  8009  opiota  8012  fmpox  8020  oalimcl  8495  oeeui  8538  nnmword  8569  isinf  9175  elfi  9326  brwdomn0  9484  alephval3  10032  dfac2b  10053  fin17  10316  isfin7-2  10318  ltmpi  10827  addclprlem1  10939  distrlem4pr  10949  1idpr  10952  qreccl  12919  0fz1  13498  zmodid2  13858  ccatrcl1  14557  eqwrds3  14923  divgcdcoprm0  16634  sscntz  19301  gexdvds  19559  rngcinv  20614  psdmvr  22135  cnprest  23254  txrest  23596  ptrescn  23604  flimrest  23948  txflf  23971  fclsrest  23989  tsmssubm  24108  mbfi1fseqlem4  25685  2sq2  27396  axcontlem7  29039  uhgreq12g  29134  nbuhgr2vtx1edgb  29421  wlkcomp  29699  uhgrwkspthlem2  29822  clwlkcomp  29847  wlknwwlksnbij  29956  hashecclwwlkn1  30147  umgrhashecclwwlk  30148  numclwwlk1lem2fo  30428  ubthlem1  30941  pjimai  32247  atcv1  32451  chirredi  32465  mplvrpmrhm  33691  bj-restsn  37394  fvineqsneu  37727  pibt2  37733  wl-sbcom2d-lem1  37884  wl-sbalnae  37887  ptrest  37940  poimirlem28  37969  heicant  37976  ftc1anclem1  38014  sbeqi  38480  ralbi12f  38481  iineq12f  38485  brcnvepres  38593  elrnressn  38601  qmapeldisjsim  39181  tfsconcat0i  43773  nzss  44744  sinnpoly  47339  or2expropbilem1  47480  modmkpkne  47815  ich2exprop  47931  ichnreuop  47932  ichreuopeq  47933  reuopreuprim  47986  rngcinvALTV  48752  snlindsntorlem  48946  itscnhlc0xyqsol  49241  opndisj  49378