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  4480  mpteq12f  5187  otthg  5440  fmptsng  7124  f1oiso  7308  mpoeq123  7441  elovmporab  7615  elovmporab1w  7616  elovmporab1  7617  ovmpt3rabdm  7628  elovmpt3rab1  7629  tfindsg  7817  findsg  7853  dfoprab4f  8014  opiota  8017  fmpox  8025  oalimcl  8501  oeeui  8543  nnmword  8574  isinf  9183  isinfOLD  9184  elfi  9340  brwdomn0  9498  alephval3  10039  dfac2b  10060  fin17  10323  isfin7-2  10325  ltmpi  10833  addclprlem1  10945  distrlem4pr  10955  1idpr  10958  qreccl  12904  0fz1  13481  zmodid2  13837  ccatrcl1  14535  eqwrds3  14903  divgcdcoprm0  16611  sscntz  19240  gexdvds  19498  rngcinv  20557  psdmvr  22089  cnprest  23209  txrest  23551  ptrescn  23559  flimrest  23903  txflf  23926  fclsrest  23944  tsmssubm  24063  mbfi1fseqlem4  25652  2sq2  27377  axcontlem7  28950  uhgreq12g  29045  nbuhgr2vtx1edgb  29332  wlkcomp  29611  uhgrwkspthlem2  29734  clwlkcomp  29759  wlknwwlksnbij  29868  hashecclwwlkn1  30056  umgrhashecclwwlk  30057  numclwwlk1lem2fo  30337  ubthlem1  30849  pjimai  32155  atcv1  32359  chirredi  32373  bj-restsn  37063  fvineqsneu  37392  pibt2  37398  wl-sbcom2d-lem1  37540  wl-sbalnae  37543  ptrest  37606  poimirlem28  37635  heicant  37642  ftc1anclem1  37680  sbeqi  38146  ralbi12f  38147  iineq12f  38151  brcnvepres  38249  elrnressn  38255  tfsconcat0i  43327  nzss  44299  sinnpoly  46885  or2expropbilem1  47026  modmkpkne  47355  ich2exprop  47465  ichnreuop  47466  ichreuopeq  47467  reuopreuprim  47520  rngcinvALTV  48257  snlindsntorlem  48452  itscnhlc0xyqsol  48747  opndisj  48884