Theorem sylan9bbr 500

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 382

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 197  df-an 383

This theorem is referenced by:  pm5.75  1014  sbcom2  2593  sbal1  2608  sbal2  2609  mpteq12f  4865  otthg  5081  fmptsng  6578  f1oiso  6744  mpt2eq123  6861  elovmpt2rab  7027  elovmpt2rab1  7028  ovmpt3rabdm  7039  elovmpt3rab1  7040  tfindsg  7207  findsg  7240  dfoprab4f  7375  opiota  7378  fmpt2x  7386  oalimcl  7794  oeeui  7836  nnmword  7867  isinf  8329  elfi  8475  brwdomn0  8630  alephval3  9133  dfac2b  9153  dfac2OLD  9155  fin17  9418  isfin7-2  9420  ltmpi  9928  addclprlem1  10040  distrlem4pr  10050  1idpr  10053  qreccl  12011  0fz1  12568  zmodid2  12906  ccatrcl1  13576  eqwrds3  13914  divgcdcoprm0  15586  sscntz  17966  gexdvds  18206  cnprest  21314  txrest  21655  ptrescn  21663  flimrest  22007  txflf  22030  fclsrest  22048  tsmssubm  22166  mbfi1fseqlem4  23705  axcontlem7  26071  uhgreq12g  26181  nbuhgr2vtx1edgb  26471  wlkcomp  26761  uhgrwkspthlem2  26885  clwlkcomp  26910  wlknwwlksnbij  27026  hashecclwwlkn1  27235  umgrhashecclwwlk  27236  numclwwlk1lem2fo  27544  ubthlem1  28066  pjimai  29375  atcv1  29579  chirredi  29593  bj-restsn  33367  wl-sbcom2d-lem1  33676  wl-sbalnae  33679  ptrest  33741  poimirlem28  33770  heicant  33777  ftc1anclem1  33817  sbeqi  34300  ralbi12f  34301  iineq12f  34305  brcnvepres  34376  nzss  39042  raaan2  41695  rngcinv  42509  rngcinvALTV  42521  ringcinv  42560  ringcinvALTV  42584  snlindsntorlem  42787