Theorem sylan9bbr 509

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  bimsc1  842  pm5.75  1026  sbcom2  2162  sbal1  2521  sbal2  2522  raaan2  4526  mpteq12f  5237  otthg  5487  fmptsng  7177  f1oiso  7358  mpoeq123  7492  elovmporab  7667  elovmporab1w  7668  elovmporab1  7669  ovmpt3rabdm  7680  elovmpt3rab1  7681  tfindsg  7866  findsg  7905  dfoprab4f  8061  opiota  8064  fmpox  8072  oalimcl  8581  oeeui  8623  nnmword  8654  isinf  9285  isinfOLD  9286  elfi  9438  brwdomn0  9594  alephval3  10135  dfac2b  10155  fin17  10419  isfin7-2  10421  ltmpi  10929  addclprlem1  11041  distrlem4pr  11051  1idpr  11054  qreccl  12986  0fz1  13556  zmodid2  13900  ccatrcl1  14580  eqwrds3  14948  divgcdcoprm0  16639  sscntz  19289  gexdvds  19551  rngcinv  20582  cnprest  23237  txrest  23579  ptrescn  23587  flimrest  23931  txflf  23954  fclsrest  23972  tsmssubm  24091  mbfi1fseqlem4  25692  2sq2  27411  axcontlem7  28853  uhgreq12g  28950  nbuhgr2vtx1edgb  29237  wlkcomp  29517  uhgrwkspthlem2  29640  clwlkcomp  29665  wlknwwlksnbij  29771  hashecclwwlkn1  29959  umgrhashecclwwlk  29960  numclwwlk1lem2fo  30240  ubthlem1  30752  pjimai  32058  atcv1  32262  chirredi  32276  bj-restsn  36689  fvineqsneu  37018  pibt2  37024  wl-sbcom2d-lem1  37154  wl-sbalnae  37157  ptrest  37220  poimirlem28  37249  heicant  37256  ftc1anclem1  37294  sbeqi  37760  ralbi12f  37761  iineq12f  37765  brcnvepres  37866  elrnressn  37872  tfsconcat0i  42913  nzss  43893  or2expropbilem1  46549  ich2exprop  46945  ichnreuop  46946  ichreuopeq  46947  reuopreuprim  47000  rngcinvALTV  47521  snlindsntorlem  47721  itscnhlc0xyqsol  48021  opndisj  48104