Theorem sylan9bbr 511

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

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

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 397

This theorem is referenced by:  bimsc1  842  pm5.75  1027  sbcom2  2161  sbal1  2526  sbal2  2527  raaan2  4487  mpteq12f  5198  otthg  5447  fmptsng  7119  f1oiso  7301  mpoeq123  7434  elovmporab  7604  elovmporab1w  7605  elovmporab1  7606  ovmpt3rabdm  7617  elovmpt3rab1  7618  tfindsg  7802  findsg  7841  dfoprab4f  7993  opiota  7996  fmpox  8004  oalimcl  8512  oeeui  8554  nnmword  8585  isinf  9211  isinfOLD  9212  elfi  9358  brwdomn0  9514  alephval3  10055  dfac2b  10075  fin17  10339  isfin7-2  10341  ltmpi  10849  addclprlem1  10961  distrlem4pr  10971  1idpr  10974  qreccl  12903  0fz1  13471  zmodid2  13814  ccatrcl1  14494  eqwrds3  14862  divgcdcoprm0  16552  sscntz  19120  gexdvds  19380  cnprest  22677  txrest  23019  ptrescn  23027  flimrest  23371  txflf  23394  fclsrest  23412  tsmssubm  23531  mbfi1fseqlem4  25120  2sq2  26818  axcontlem7  27982  uhgreq12g  28079  nbuhgr2vtx1edgb  28363  wlkcomp  28642  uhgrwkspthlem2  28765  clwlkcomp  28790  wlknwwlksnbij  28896  hashecclwwlkn1  29084  umgrhashecclwwlk  29085  numclwwlk1lem2fo  29365  ubthlem1  29875  pjimai  31181  atcv1  31385  chirredi  31399  bj-restsn  35626  fvineqsneu  35955  pibt2  35961  wl-sbcom2d-lem1  36087  wl-sbalnae  36090  ptrest  36150  poimirlem28  36179  heicant  36186  ftc1anclem1  36224  sbeqi  36691  ralbi12f  36692  iineq12f  36696  brcnvepres  36800  elrnressn  36806  tfsconcat0i  41738  nzss  42719  or2expropbilem1  45386  ich2exprop  45783  ichnreuop  45784  ichreuopeq  45785  reuopreuprim  45838  rngcinv  46399  rngcinvALTV  46411  snlindsntorlem  46671  itscnhlc0xyqsol  46971  opndisj  47055