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  2209  sbal1  2559  sbal2  2560  raaan2  4481  mpteq12f  5194  otthg  5465  dm0rn0  5912  fmptsng  7169  f1oiso  7355  mpoeq123  7488  elovmporab  7663  elovmporab1w  7664  elovmporab1  7665  ovmpt3rabdm  7676  elovmpt3rab1  7677  tfindsg  7860  findsg  7897  dfoprab4f  8056  opiota  8059  fmpox  8067  oalimcl  8550  oeeui  8593  nnmword  8624  isinf  9238  elfi  9386  brwdomn0  9544  alephval3  10116  dfac2b  10136  fin17  10399  isfin7-2  10401  ltmpi  10914  addclprlem1  11026  distrlem4pr  11036  1idpr  11039  qreccl  13019  0fz1  13598  zmodid2  13960  ccatrcl1  14661  eqwrds3  15034  divgcdcoprm0  16757  sscntz  19452  gexdvds  19710  rngcinv  20798  psdmvr  22396  cnprest  23513  txrest  23856  ptrescn  23864  flimrest  24208  txflf  24231  fclsrest  24249  tsmssubm  24368  mbfi1fseqlem4  25945  2sq2  27665  axcontlem7  29411  uhgreq12g  29506  nbuhgr2vtx1edgb  29796  wlkcomp  30074  uhgrwkspthlem2  30203  clwlkcomp  30229  wlknwwlksnbij  30340  hashecclwwlkn1  30531  umgrhashecclwwlk  30532  numclwwlk1lem2fo  30822  ubthlem1  31335  pjimai  32641  atcv1  32845  chirredi  32859  mplvrpmrhm  34042  bj-restsn  37817  fvineqsneu  38150  pibt2  38156  wl-sbcom2d-lem1  38307  wl-sbalnae  38310  ptrest  38353  poimirlem28  38382  heicant  38389  ftc1anclem1  38427  sbeqi  38892  ralbi12f  38893  iineq12f  38897  brcnvepres  39005  elrnressn  39013  qmapeldisjsim  39593  tfsconcat0i  44171  nzss  45126  sinnpoly  47744  or2expropbilem1  47905  modmkpkne  48240  ich2exprop  48356  ichnreuop  48357  ichreuopeq  48358  reuopreuprim  48411  rngcinvALTV  49176  snlindsntorlem  49385  itscnhlc0xyqsol  49680  opndisj  49814