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  845  pm5.75  1031  sbcom2  2179  sbal1  2533  sbal2  2534  raaan2  4463  mpteq12f  5171  otthg  5435  dm0rn0  5875  fmptsng  7118  f1oiso  7301  mpoeq123  7434  elovmporab  7608  elovmporab1w  7609  elovmporab1  7610  ovmpt3rabdm  7621  elovmpt3rab1  7622  tfindsg  7807  findsg  7843  dfoprab4f  8004  opiota  8007  fmpox  8015  oalimcl  8490  oeeui  8533  nnmword  8564  isinf  9170  elfi  9321  brwdomn0  9479  alephval3  10027  dfac2b  10048  fin17  10311  isfin7-2  10313  ltmpi  10822  addclprlem1  10934  distrlem4pr  10944  1idpr  10947  qreccl  12914  0fz1  13493  zmodid2  13853  ccatrcl1  14552  eqwrds3  14918  divgcdcoprm0  16629  sscntz  19296  gexdvds  19554  rngcinv  20609  psdmvr  22149  cnprest  23268  txrest  23610  ptrescn  23618  flimrest  23962  txflf  23985  fclsrest  24003  tsmssubm  24122  mbfi1fseqlem4  25699  2sq2  27414  axcontlem7  29057  uhgreq12g  29152  nbuhgr2vtx1edgb  29439  wlkcomp  29718  uhgrwkspthlem2  29841  clwlkcomp  29866  wlknwwlksnbij  29975  hashecclwwlkn1  30166  umgrhashecclwwlk  30167  numclwwlk1lem2fo  30447  ubthlem1  30960  pjimai  32266  atcv1  32470  chirredi  32484  mplvrpmrhm  33710  bj-restsn  37414  fvineqsneu  37745  pibt2  37751  wl-sbcom2d-lem1  37902  wl-sbalnae  37905  ptrest  37958  poimirlem28  37987  heicant  37994  ftc1anclem1  38032  sbeqi  38498  ralbi12f  38499  iineq12f  38503  brcnvepres  38611  elrnressn  38619  qmapeldisjsim  39199  tfsconcat0i  43795  nzss  44766  sinnpoly  47355  or2expropbilem1  47496  modmkpkne  47831  ich2exprop  47947  ichnreuop  47948  ichreuopeq  47949  reuopreuprim  48002  rngcinvALTV  48768  snlindsntorlem  48962  itscnhlc0xyqsol  49257  opndisj  49394