Theorem sylan9bbr 519

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 518	. 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏))
4	3	ancoms 463	1 ⊢ ((𝜃 ∧ 𝜑) → (𝜓 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  bimsc1  857  pm5.75  1044  sbcom2  2213  sbal1  2566  sbal2  2567  raaan2  4488  mpteq12f  5200  otthg  5470  dm0rn0  5917  fmptsng  7169  f1oiso  7352  mpoeq123  7485  elovmporab  7659  elovmporab1w  7660  elovmporab1  7661  ovmpt3rabdm  7672  elovmpt3rab1  7673  tfindsg  7859  findsg  7896  dfoprab4f  8055  opiota  8058  fmpox  8066  oalimcl  8547  oeeui  8590  nnmword  8621  isinf  9227  elfi  9375  brwdomn0  9533  alephval3  10096  dfac2b  10116  fin17  10380  isfin7-2  10382  ltmpi  10891  addclprlem1  11003  distrlem4pr  11013  1idpr  11016  qreccl  12995  0fz1  13574  zmodid2  13934  ccatrcl1  14634  eqwrds3  15000  divgcdcoprm0  16725  sscntz  19398  gexdvds  19656  rngcinv  20724  psdmvr  22303  cnprest  23417  txrest  23759  ptrescn  23767  flimrest  24111  txflf  24134  fclsrest  24152  tsmssubm  24271  mbfi1fseqlem4  25848  2sq2  27565  axcontlem7  29263  uhgreq12g  29358  nbuhgr2vtx1edgb  29645  wlkcomp  29923  uhgrwkspthlem2  30046  clwlkcomp  30071  wlknwwlksnbij  30180  hashecclwwlkn1  30371  umgrhashecclwwlk  30372  numclwwlk1lem2fo  30652  ubthlem1  31165  pjimai  32471  atcv1  32675  chirredi  32689  mplvrpmrhm  33884  bj-restsn  37649  fvineqsneu  37982  pibt2  37988  wl-sbcom2d-lem1  38139  wl-sbalnae  38142  ptrest  38195  poimirlem28  38224  heicant  38231  ftc1anclem1  38269  sbeqi  38735  ralbi12f  38736  iineq12f  38740  brcnvepres  38848  elrnressn  38856  qmapeldisjsim  39436  tfsconcat0i  44001  nzss  44956  sinnpoly  47554  or2expropbilem1  47695  modmkpkne  48030  ich2exprop  48146  ichnreuop  48147  ichreuopeq  48148  reuopreuprim  48201  rngcinvALTV  48967  snlindsntorlem  49172  itscnhlc0xyqsol  49467  opndisj  49603