Theorem sylan9bbr 737

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

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

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 386

This theorem is referenced by:  pm5.75  978  pm5.75OLD  979  sbcom2  2445  sbal1  2460  sbal2  2461  mpteq12f  4731  otthg  4954  fmptsng  6434  f1oiso  6601  mpt2eq123  6714  elovmpt2rab  6880  elovmpt2rab1  6881  ovmpt3rabdm  6892  elovmpt3rab1  6893  tfindsg  7060  findsg  7093  dfoprab4f  7226  opiota  7229  fmpt2x  7236  oalimcl  7640  oeeui  7682  nnmword  7713  isinf  8173  elfi  8319  brwdomn0  8474  alephval3  8933  dfac2  8953  fin17  9216  isfin7-2  9218  ltmpi  9726  addclprlem1  9838  distrlem4pr  9848  1idpr  9851  qreccl  11808  0fz1  12361  zmodid2  12698  ccatrcl1  13376  eqwrds3  13704  divgcdcoprm0  15379  sscntz  17759  gexdvds  17999  cnprest  21093  txrest  21434  ptrescn  21442  flimrest  21787  txflf  21810  fclsrest  21828  tsmssubm  21946  mbfi1fseqlem4  23485  axcontlem7  25850  uhgreq12g  25960  nbuhgr2vtx1edgb  26248  wlkcomp  26526  uhgrwkspthlem2  26650  clwlkcomp  26675  hashecclwwlksn1  26954  umgrhashecclwwlk  26955  numclwlk1lem2fo  27228  ubthlem1  27726  pjimai  29035  atcv1  29239  chirredi  29253  bj-restsn  33035  wl-sbcom2d-lem1  33342  wl-sbalnae  33345  ptrest  33408  poimirlem28  33437  heicant  33444  ftc1anclem1  33485  sbeqi  33968  ralbi12f  33969  iineq12f  33973  brcnvepres  34033  nzss  38516  raaan2  41175  rngcinv  41981  rngcinvALTV  41993  ringcinv  42032  ringcinvALTV  42056  snlindsntorlem  42259