Theorem sylan9bbr 516

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 397

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 209  df-an 398

This theorem is referenced by:  bimsc1  851  pm5.75  1037  sbcom2  2185  sbal1  2538  sbal2  2539  raaan2  4453  mpteq12f  5160  otthg  5428  dm0rn0  5873  fmptsng  7116  f1oiso  7299  mpoeq123  7432  elovmporab  7606  elovmporab1w  7607  elovmporab1  7608  ovmpt3rabdm  7619  elovmpt3rab1  7620  tfindsg  7805  findsg  7841  dfoprab4f  8002  opiota  8005  fmpox  8013  oalimcl  8489  oeeui  8532  nnmword  8563  isinf  9169  elfi  9320  brwdomn0  9478  alephval3  10027  dfac2b  10048  fin17  10311  isfin7-2  10313  ltmpi  10822  addclprlem1  10934  distrlem4pr  10944  1idpr  10947  qreccl  12914  0fz1  13493  zmodid2  13853  ccatrcl1  14552  eqwrds3  14918  divgcdcoprm0  16629  sscntz  19296  gexdvds  19554  rngcinv  20613  psdmvr  22161  cnprest  23276  txrest  23618  ptrescn  23626  flimrest  23970  txflf  23993  fclsrest  24011  tsmssubm  24130  mbfi1fseqlem4  25707  2sq2  27418  axcontlem7  29061  uhgreq12g  29156  nbuhgr2vtx1edgb  29443  wlkcomp  29721  uhgrwkspthlem2  29844  clwlkcomp  29869  wlknwwlksnbij  29978  hashecclwwlkn1  30169  umgrhashecclwwlk  30170  numclwwlk1lem2fo  30450  ubthlem1  30963  pjimai  32269  atcv1  32473  chirredi  32487  mplvrpmrhm  33743  bj-restsn  37455  fvineqsneu  37788  pibt2  37794  wl-sbcom2d-lem1  37945  wl-sbalnae  37948  ptrest  38001  poimirlem28  38030  heicant  38037  ftc1anclem1  38075  sbeqi  38541  ralbi12f  38542  iineq12f  38546  brcnvepres  38654  elrnressn  38662  qmapeldisjsim  39242  tfsconcat0i  43805  nzss  44776  sinnpoly  47368  or2expropbilem1  47509  modmkpkne  47844  ich2exprop  47960  ichnreuop  47961  ichreuopeq  47962  reuopreuprim  48015  rngcinvALTV  48781  snlindsntorlem  48975  itscnhlc0xyqsol  49270  opndisj  49407