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  2172  sbal1  2532  sbal2  2533  raaan2  4520  mpteq12f  5229  otthg  5489  fmptsng  7189  f1oiso  7372  mpoeq123  7506  elovmporab  7680  elovmporab1w  7681  elovmporab1  7682  ovmpt3rabdm  7693  elovmpt3rab1  7694  tfindsg  7883  findsg  7920  dfoprab4f  8082  opiota  8085  fmpox  8093  oalimcl  8599  oeeui  8641  nnmword  8672  isinf  9297  isinfOLD  9298  elfi  9454  brwdomn0  9610  alephval3  10151  dfac2b  10172  fin17  10435  isfin7-2  10437  ltmpi  10945  addclprlem1  11057  distrlem4pr  11067  1idpr  11070  qreccl  13012  0fz1  13585  zmodid2  13940  ccatrcl1  14633  eqwrds3  15001  divgcdcoprm0  16703  sscntz  19345  gexdvds  19603  rngcinv  20638  psdmvr  22174  cnprest  23298  txrest  23640  ptrescn  23648  flimrest  23992  txflf  24015  fclsrest  24033  tsmssubm  24152  mbfi1fseqlem4  25754  2sq2  27478  axcontlem7  28986  uhgreq12g  29083  nbuhgr2vtx1edgb  29370  wlkcomp  29650  uhgrwkspthlem2  29775  clwlkcomp  29800  wlknwwlksnbij  29909  hashecclwwlkn1  30097  umgrhashecclwwlk  30098  numclwwlk1lem2fo  30378  ubthlem1  30890  pjimai  32196  atcv1  32400  chirredi  32414  bj-restsn  37084  fvineqsneu  37413  pibt2  37419  wl-sbcom2d-lem1  37561  wl-sbalnae  37564  ptrest  37627  poimirlem28  37656  heicant  37663  ftc1anclem1  37701  sbeqi  38167  ralbi12f  38168  iineq12f  38172  brcnvepres  38269  elrnressn  38275  tfsconcat0i  43363  nzss  44341  or2expropbilem1  47049  ich2exprop  47463  ichnreuop  47464  ichreuopeq  47465  reuopreuprim  47518  rngcinvALTV  48197  snlindsntorlem  48392  itscnhlc0xyqsol  48691  opndisj  48807