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  2527  sbal2  2528  raaan2  4486  mpteq12f  5194  otthg  5447  fmptsng  7144  f1oiso  7328  mpoeq123  7463  elovmporab  7637  elovmporab1w  7638  elovmporab1  7639  ovmpt3rabdm  7650  elovmpt3rab1  7651  tfindsg  7839  findsg  7875  dfoprab4f  8037  opiota  8040  fmpox  8048  oalimcl  8526  oeeui  8568  nnmword  8599  isinf  9213  isinfOLD  9214  elfi  9370  brwdomn0  9528  alephval3  10069  dfac2b  10090  fin17  10353  isfin7-2  10355  ltmpi  10863  addclprlem1  10975  distrlem4pr  10985  1idpr  10988  qreccl  12934  0fz1  13511  zmodid2  13867  ccatrcl1  14565  eqwrds3  14933  divgcdcoprm0  16641  sscntz  19264  gexdvds  19520  rngcinv  20552  psdmvr  22062  cnprest  23182  txrest  23524  ptrescn  23532  flimrest  23876  txflf  23899  fclsrest  23917  tsmssubm  24036  mbfi1fseqlem4  25625  2sq2  27350  axcontlem7  28903  uhgreq12g  28998  nbuhgr2vtx1edgb  29285  wlkcomp  29565  uhgrwkspthlem2  29690  clwlkcomp  29715  wlknwwlksnbij  29824  hashecclwwlkn1  30012  umgrhashecclwwlk  30013  numclwwlk1lem2fo  30293  ubthlem1  30805  pjimai  32111  atcv1  32315  chirredi  32329  bj-restsn  37065  fvineqsneu  37394  pibt2  37400  wl-sbcom2d-lem1  37542  wl-sbalnae  37545  ptrest  37608  poimirlem28  37637  heicant  37644  ftc1anclem1  37682  sbeqi  38148  ralbi12f  38149  iineq12f  38153  brcnvepres  38251  elrnressn  38257  tfsconcat0i  43327  nzss  44299  or2expropbilem1  47023  modmkpkne  47352  ich2exprop  47462  ichnreuop  47463  ichreuopeq  47464  reuopreuprim  47517  rngcinvALTV  48254  snlindsntorlem  48449  itscnhlc0xyqsol  48744  opndisj  48879