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  845  pm5.75  1031  sbcom2  2179  sbal1  2533  sbal2  2534  raaan2  4477  mpteq12f  5185  otthg  5443  dm0rn0  5883  fmptsng  7126  f1oiso  7309  mpoeq123  7442  elovmporab  7616  elovmporab1w  7617  elovmporab1  7618  ovmpt3rabdm  7629  elovmpt3rab1  7630  tfindsg  7815  findsg  7851  dfoprab4f  8012  opiota  8015  fmpox  8023  oalimcl  8499  oeeui  8542  nnmword  8573  isinf  9179  elfi  9330  brwdomn0  9488  alephval3  10034  dfac2b  10055  fin17  10318  isfin7-2  10320  ltmpi  10829  addclprlem1  10941  distrlem4pr  10951  1idpr  10954  qreccl  12896  0fz1  13474  zmodid2  13833  ccatrcl1  14532  eqwrds3  14898  divgcdcoprm0  16606  sscntz  19272  gexdvds  19530  rngcinv  20587  psdmvr  22129  cnprest  23250  txrest  23592  ptrescn  23600  flimrest  23944  txflf  23967  fclsrest  23985  tsmssubm  24104  mbfi1fseqlem4  25692  2sq2  27417  axcontlem7  29061  uhgreq12g  29156  nbuhgr2vtx1edgb  29443  wlkcomp  29722  uhgrwkspthlem2  29845  clwlkcomp  29870  wlknwwlksnbij  29979  hashecclwwlkn1  30170  umgrhashecclwwlk  30171  numclwwlk1lem2fo  30451  ubthlem1  30964  pjimai  32270  atcv1  32474  chirredi  32488  mplvrpmrhm  33730  bj-restsn  37362  fvineqsneu  37693  pibt2  37699  wl-sbcom2d-lem1  37843  wl-sbalnae  37846  ptrest  37899  poimirlem28  37928  heicant  37935  ftc1anclem1  37973  sbeqi  38439  ralbi12f  38440  iineq12f  38444  brcnvepres  38552  elrnressn  38560  qmapeldisjsim  39140  tfsconcat0i  43731  nzss  44702  sinnpoly  47280  or2expropbilem1  47421  modmkpkne  47750  ich2exprop  47860  ichnreuop  47861  ichreuopeq  47862  reuopreuprim  47915  rngcinvALTV  48665  snlindsntorlem  48859  itscnhlc0xyqsol  49154  opndisj  49291