Theorem sylan9bbr 512

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  bimsc1  843  pm5.75  1028  sbcom2  2162  sbal1  2528  sbal2  2529  raaan2  4525  mpteq12f  5237  otthg  5486  fmptsng  7166  f1oiso  7348  mpoeq123  7481  elovmporab  7652  elovmporab1w  7653  elovmporab1  7654  ovmpt3rabdm  7665  elovmpt3rab1  7666  tfindsg  7850  findsg  7890  dfoprab4f  8042  opiota  8045  fmpox  8053  oalimcl  8560  oeeui  8602  nnmword  8633  isinf  9260  isinfOLD  9261  elfi  9408  brwdomn0  9564  alephval3  10105  dfac2b  10125  fin17  10389  isfin7-2  10391  ltmpi  10899  addclprlem1  11011  distrlem4pr  11021  1idpr  11024  qreccl  12953  0fz1  13521  zmodid2  13864  ccatrcl1  14544  eqwrds3  14912  divgcdcoprm0  16602  sscntz  19190  gexdvds  19452  cnprest  22793  txrest  23135  ptrescn  23143  flimrest  23487  txflf  23510  fclsrest  23528  tsmssubm  23647  mbfi1fseqlem4  25236  2sq2  26936  axcontlem7  28228  uhgreq12g  28325  nbuhgr2vtx1edgb  28609  wlkcomp  28888  uhgrwkspthlem2  29011  clwlkcomp  29036  wlknwwlksnbij  29142  hashecclwwlkn1  29330  umgrhashecclwwlk  29331  numclwwlk1lem2fo  29611  ubthlem1  30123  pjimai  31429  atcv1  31633  chirredi  31647  bj-restsn  35963  fvineqsneu  36292  pibt2  36298  wl-sbcom2d-lem1  36424  wl-sbalnae  36427  ptrest  36487  poimirlem28  36516  heicant  36523  ftc1anclem1  36561  sbeqi  37027  ralbi12f  37028  iineq12f  37032  brcnvepres  37135  elrnressn  37141  tfsconcat0i  42095  nzss  43076  or2expropbilem1  45742  ich2exprop  46139  ichnreuop  46140  ichreuopeq  46141  reuopreuprim  46194  rngcinv  46879  rngcinvALTV  46891  snlindsntorlem  47151  itscnhlc0xyqsol  47451  opndisj  47535