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  841  pm5.75  1026  sbcom2  2161  sbal1  2533  sbal2  2534  raaan2  4455  mpteq12f  5162  otthg  5400  fmptsng  7040  f1oiso  7222  mpoeq123  7347  elovmporab  7515  elovmporab1w  7516  elovmporab1  7517  ovmpt3rabdm  7528  elovmpt3rab1  7529  tfindsg  7707  findsg  7746  dfoprab4f  7896  opiota  7899  fmpox  7907  oalimcl  8391  oeeui  8433  nnmword  8464  isinf  9036  elfi  9172  brwdomn0  9328  alephval3  9866  dfac2b  9886  fin17  10150  isfin7-2  10152  ltmpi  10660  addclprlem1  10772  distrlem4pr  10782  1idpr  10785  qreccl  12709  0fz1  13276  zmodid2  13619  ccatrcl1  14299  eqwrds3  14676  divgcdcoprm0  16370  sscntz  18932  gexdvds  19189  cnprest  22440  txrest  22782  ptrescn  22790  flimrest  23134  txflf  23157  fclsrest  23175  tsmssubm  23294  mbfi1fseqlem4  24883  2sq2  26581  axcontlem7  27338  uhgreq12g  27435  nbuhgr2vtx1edgb  27719  wlkcomp  27998  uhgrwkspthlem2  28122  clwlkcomp  28147  wlknwwlksnbij  28253  hashecclwwlkn1  28441  umgrhashecclwwlk  28442  numclwwlk1lem2fo  28722  ubthlem1  29232  pjimai  30538  atcv1  30742  chirredi  30756  bj-restsn  35253  fvineqsneu  35582  pibt2  35588  wl-sbcom2d-lem1  35714  wl-sbalnae  35717  ptrest  35776  poimirlem28  35805  heicant  35812  ftc1anclem1  35850  sbeqi  36317  ralbi12f  36318  iineq12f  36322  brcnvepres  36406  nzss  41935  or2expropbilem1  44526  ich2exprop  44923  ichnreuop  44924  ichreuopeq  44925  reuopreuprim  44978  rngcinv  45539  rngcinvALTV  45551  ringcinv  45590  ringcinvALTV  45614  snlindsntorlem  45811  itscnhlc0xyqsol  46111  opndisj  46196