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 205   ∧ 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 206  df-an 396

This theorem is referenced by:  bimsc1  840  pm5.75  1025  sbcom2  2163  sbal1  2533  sbal2  2534  raaan2  4452  mpteq12f  5158  otthg  5394  fmptsng  7022  f1oiso  7202  mpoeq123  7325  elovmporab  7493  elovmporab1w  7494  elovmporab1  7495  ovmpt3rabdm  7506  elovmpt3rab1  7507  tfindsg  7682  findsg  7720  dfoprab4f  7869  opiota  7872  fmpox  7880  oalimcl  8353  oeeui  8395  nnmword  8426  isinf  8965  elfi  9102  brwdomn0  9258  alephval3  9797  dfac2b  9817  fin17  10081  isfin7-2  10083  ltmpi  10591  addclprlem1  10703  distrlem4pr  10713  1idpr  10716  qreccl  12638  0fz1  13205  zmodid2  13547  ccatrcl1  14227  eqwrds3  14604  divgcdcoprm0  16298  sscntz  18847  gexdvds  19104  cnprest  22348  txrest  22690  ptrescn  22698  flimrest  23042  txflf  23065  fclsrest  23083  tsmssubm  23202  mbfi1fseqlem4  24788  2sq2  26486  axcontlem7  27241  uhgreq12g  27338  nbuhgr2vtx1edgb  27622  wlkcomp  27900  uhgrwkspthlem2  28023  clwlkcomp  28048  wlknwwlksnbij  28154  hashecclwwlkn1  28342  umgrhashecclwwlk  28343  numclwwlk1lem2fo  28623  ubthlem1  29133  pjimai  30439  atcv1  30643  chirredi  30657  bj-restsn  35180  fvineqsneu  35509  pibt2  35515  wl-sbcom2d-lem1  35641  wl-sbalnae  35644  ptrest  35703  poimirlem28  35732  heicant  35739  ftc1anclem1  35777  sbeqi  36244  ralbi12f  36245  iineq12f  36249  brcnvepres  36333  nzss  41824  or2expropbilem1  44413  ich2exprop  44811  ichnreuop  44812  ichreuopeq  44813  reuopreuprim  44866  rngcinv  45427  rngcinvALTV  45439  ringcinv  45478  ringcinvALTV  45502  snlindsntorlem  45699  itscnhlc0xyqsol  45999  opndisj  46084