Theorem sylan9bbr 519

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401

This theorem is used by:  bimsc1  857  pm5.75  1046  sbcom2  2207  sbal1  2560  sbal2  2561  raaan2  4483  mpteq12f  5196  otthg  5467  dm0rn0  5914  fmptsng  7166  f1oiso  7349  mpoeq123  7482  elovmporab  7656  elovmporab1w  7657  elovmporab1  7658  ovmpt3rabdm  7669  elovmpt3rab1  7670  tfindsg  7853  findsg  7890  dfoprab4f  8049  opiota  8052  fmpox  8060  oalimcl  8541  oeeui  8584  nnmword  8615  isinf  9221  elfi  9369  brwdomn0  9527  alephval3  10099  dfac2b  10119  fin17  10382  isfin7-2  10384  ltmpi  10893  addclprlem1  11005  distrlem4pr  11015  1idpr  11018  qreccl  12997  0fz1  13576  zmodid2  13937  ccatrcl1  14637  eqwrds3  15003  divgcdcoprm0  16727  sscntz  19400  gexdvds  19658  rngcinv  20745  psdmvr  22341  cnprest  23455  txrest  23797  ptrescn  23805  flimrest  24149  txflf  24172  fclsrest  24190  tsmssubm  24309  mbfi1fseqlem4  25886  2sq2  27606  axcontlem7  29329  uhgreq12g  29424  nbuhgr2vtx1edgb  29711  wlkcomp  29989  uhgrwkspthlem2  30112  clwlkcomp  30137  wlknwwlksnbij  30246  hashecclwwlkn1  30437  umgrhashecclwwlk  30438  numclwwlk1lem2fo  30718  ubthlem1  31231  pjimai  32537  atcv1  32741  chirredi  32755  mplvrpmrhm  33946  bj-restsn  37752  fvineqsneu  38085  pibt2  38091  wl-sbcom2d-lem1  38242  wl-sbalnae  38245  ptrest  38298  poimirlem28  38327  heicant  38334  ftc1anclem1  38372  sbeqi  38836  ralbi12f  38837  iineq12f  38841  brcnvepres  38949  elrnressn  38957  qmapeldisjsim  39537  tfsconcat0i  44100  nzss  45055  sinnpoly  47656  or2expropbilem1  47797  modmkpkne  48132  ich2exprop  48248  ichnreuop  48249  ichreuopeq  48250  reuopreuprim  48303  rngcinvALTV  49069  snlindsntorlem  49278  itscnhlc0xyqsol  49573  opndisj  49709