Theorem sylan9bbr 520

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  bimsc1  858  pm5.75  1046  sbcom2  2212  sbal1  2560  sbal2  2561  raaan2  4481  mpteq12f  5193  otthg  5458  dm0rn0  5913  fmptsng  7196  f1oiso  7382  mpoeq123  7515  elovmporab  7691  elovmporab1w  7692  elovmporab1  7693  ovmpt3rabdm  7704  elovmpt3rab1  7705  tfindsg  7896  findsg  7933  dfoprab4f  8092  opiota  8095  fmpox  8103  oalimcl  8596  oeeui  8639  nnmword  8670  isinf  9284  elfi  9432  brwdomn0  9590  alephval3  10216  dfac2b  10236  fin17  10499  isfin7-2  10501  ltmpi  11016  addclprlem1  11128  distrlem4pr  11138  1idpr  11141  qreccl  13124  0fz1  13704  zmodid2  14066  ccatrcl1  14768  eqwrds3  15143  divgcdcoprm0  16869  sscntz  19570  gexdvds  19828  rngcinv  20919  psdmvr  22520  cnprest  23637  txrest  23980  ptrescn  23988  flimrest  24332  txflf  24355  fclsrest  24373  tsmssubm  24492  mbfi1fseqlem4  26069  2sq2  27790  axcontlem7  29578  uhgreq12g  29673  nbuhgr2vtx1edgb  29963  wlkcomp  30241  uhgrwkspthlem2  30370  clwlkcomp  30396  wlknwwlksnbij  30507  hashecclwwlkn1  30698  umgrhashecclwwlk  30699  numclwwlk1lem2fo  30989  ubthlem1  31502  pjimai  32808  atcv1  33012  chirredi  33026  mplvrpmrhm  34249  srepdflem1  36085  bj-restsn  38194  fvineqsneu  38526  pibt2  38532  wl-sbcom2d-lem1  38683  wl-sbalnae  38686  ptrest  38729  poimirlem28  38758  heicant  38765  ftc1anclem1  38803  sbeqi  39283  ralbi12f  39284  iineq12f  39288  brcnvepres  39396  elrnressn  39404  qmapeldisjsim  39984  tfsconcat0i  44539  nzss  45493  sinnpoly  48146  or2expropbilem1  48307  modmkpkne  48642  ich2exprop  48758  ichnreuop  48759  ichreuopeq  48760  reuopreuprim  48813  rngcinvALTV  49578  snlindsntorlem  49787  itscnhlc0xyqsol  50082  opndisj  50222