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  2526  sbal2  2527  raaan2  4472  mpteq12f  5177  otthg  5428  fmptsng  7104  f1oiso  7288  mpoeq123  7421  elovmporab  7595  elovmporab1w  7596  elovmporab1  7597  ovmpt3rabdm  7608  elovmpt3rab1  7609  tfindsg  7794  findsg  7830  dfoprab4f  7991  opiota  7994  fmpox  8002  oalimcl  8478  oeeui  8520  nnmword  8551  isinf  9154  elfi  9303  brwdomn0  9461  alephval3  10004  dfac2b  10025  fin17  10288  isfin7-2  10290  ltmpi  10798  addclprlem1  10910  distrlem4pr  10920  1idpr  10923  qreccl  12870  0fz1  13447  zmodid2  13803  ccatrcl1  14501  eqwrds3  14868  divgcdcoprm0  16576  sscntz  19205  gexdvds  19463  rngcinv  20522  psdmvr  22054  cnprest  23174  txrest  23516  ptrescn  23524  flimrest  23868  txflf  23891  fclsrest  23909  tsmssubm  24028  mbfi1fseqlem4  25617  2sq2  27342  axcontlem7  28915  uhgreq12g  29010  nbuhgr2vtx1edgb  29297  wlkcomp  29576  uhgrwkspthlem2  29699  clwlkcomp  29724  wlknwwlksnbij  29833  hashecclwwlkn1  30021  umgrhashecclwwlk  30022  numclwwlk1lem2fo  30302  ubthlem1  30814  pjimai  32120  atcv1  32324  chirredi  32338  bj-restsn  37066  fvineqsneu  37395  pibt2  37401  wl-sbcom2d-lem1  37543  wl-sbalnae  37546  ptrest  37609  poimirlem28  37638  heicant  37645  ftc1anclem1  37683  sbeqi  38149  ralbi12f  38150  iineq12f  38154  brcnvepres  38252  elrnressn  38258  tfsconcat0i  43328  nzss  44300  sinnpoly  46885  or2expropbilem1  47026  modmkpkne  47355  ich2exprop  47465  ichnreuop  47466  ichreuopeq  47467  reuopreuprim  47520  rngcinvALTV  48270  snlindsntorlem  48465  itscnhlc0xyqsol  48760  opndisj  48897