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  844  pm5.75  1030  sbcom2  2174  sbal1  2533  sbal2  2534  raaan2  4501  mpteq12f  5210  otthg  5465  fmptsng  7165  f1oiso  7349  mpoeq123  7484  elovmporab  7658  elovmporab1w  7659  elovmporab1  7660  ovmpt3rabdm  7671  elovmpt3rab1  7672  tfindsg  7861  findsg  7898  dfoprab4f  8060  opiota  8063  fmpox  8071  oalimcl  8577  oeeui  8619  nnmword  8650  isinf  9273  isinfOLD  9274  elfi  9430  brwdomn0  9588  alephval3  10129  dfac2b  10150  fin17  10413  isfin7-2  10415  ltmpi  10923  addclprlem1  11035  distrlem4pr  11045  1idpr  11048  qreccl  12990  0fz1  13566  zmodid2  13921  ccatrcl1  14617  eqwrds3  14985  divgcdcoprm0  16689  sscntz  19314  gexdvds  19570  rngcinv  20602  psdmvr  22112  cnprest  23232  txrest  23574  ptrescn  23582  flimrest  23926  txflf  23949  fclsrest  23967  tsmssubm  24086  mbfi1fseqlem4  25676  2sq2  27401  axcontlem7  28954  uhgreq12g  29049  nbuhgr2vtx1edgb  29336  wlkcomp  29616  uhgrwkspthlem2  29741  clwlkcomp  29766  wlknwwlksnbij  29875  hashecclwwlkn1  30063  umgrhashecclwwlk  30064  numclwwlk1lem2fo  30344  ubthlem1  30856  pjimai  32162  atcv1  32366  chirredi  32380  bj-restsn  37105  fvineqsneu  37434  pibt2  37440  wl-sbcom2d-lem1  37582  wl-sbalnae  37585  ptrest  37648  poimirlem28  37677  heicant  37684  ftc1anclem1  37722  sbeqi  38188  ralbi12f  38189  iineq12f  38193  brcnvepres  38290  elrnressn  38296  tfsconcat0i  43344  nzss  44316  or2expropbilem1  47041  ich2exprop  47465  ichnreuop  47466  ichreuopeq  47467  reuopreuprim  47520  rngcinvALTV  48231  snlindsntorlem  48426  itscnhlc0xyqsol  48725  opndisj  48857