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  2171  sbal1  2531  sbal2  2532  raaan2  4527  mpteq12f  5236  otthg  5496  fmptsng  7188  f1oiso  7371  mpoeq123  7505  elovmporab  7679  elovmporab1w  7680  elovmporab1  7681  ovmpt3rabdm  7692  elovmpt3rab1  7693  tfindsg  7882  findsg  7920  dfoprab4f  8080  opiota  8083  fmpox  8091  oalimcl  8597  oeeui  8639  nnmword  8670  isinf  9294  isinfOLD  9295  elfi  9451  brwdomn0  9607  alephval3  10148  dfac2b  10169  fin17  10432  isfin7-2  10434  ltmpi  10942  addclprlem1  11054  distrlem4pr  11064  1idpr  11067  qreccl  13009  0fz1  13581  zmodid2  13936  ccatrcl1  14629  eqwrds3  14997  divgcdcoprm0  16699  sscntz  19357  gexdvds  19617  rngcinv  20654  cnprest  23313  txrest  23655  ptrescn  23663  flimrest  24007  txflf  24030  fclsrest  24048  tsmssubm  24167  mbfi1fseqlem4  25768  2sq2  27492  axcontlem7  29000  uhgreq12g  29097  nbuhgr2vtx1edgb  29384  wlkcomp  29664  uhgrwkspthlem2  29787  clwlkcomp  29812  wlknwwlksnbij  29918  hashecclwwlkn1  30106  umgrhashecclwwlk  30107  numclwwlk1lem2fo  30387  ubthlem1  30899  pjimai  32205  atcv1  32409  chirredi  32423  bj-restsn  37065  fvineqsneu  37394  pibt2  37400  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  43335  nzss  44313  or2expropbilem1  46982  ich2exprop  47396  ichnreuop  47397  ichreuopeq  47398  reuopreuprim  47451  rngcinvALTV  48120  snlindsntorlem  48316  itscnhlc0xyqsol  48615  opndisj  48699