Theorem sylan9bbr 518

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  bimsc1  855  pm5.75  1042  sbcom2  2208  sbal1  2561  sbal2  2562  raaan2  4478  mpteq12f  5187  otthg  5455  dm0rn0  5902  fmptsng  7154  f1oiso  7337  mpoeq123  7470  elovmporab  7644  elovmporab1w  7645  elovmporab1  7646  ovmpt3rabdm  7657  elovmpt3rab1  7658  tfindsg  7843  findsg  7880  dfoprab4f  8039  opiota  8042  fmpox  8050  oalimcl  8531  oeeui  8574  nnmword  8605  isinf  9211  elfi  9361  brwdomn0  9519  alephval3  10068  dfac2b  10089  fin17  10353  isfin7-2  10355  ltmpi  10864  addclprlem1  10976  distrlem4pr  10986  1idpr  10989  qreccl  12972  0fz1  13551  zmodid2  13911  ccatrcl1  14610  eqwrds3  14976  divgcdcoprm0  16701  sscntz  19368  gexdvds  19626  rngcinv  20689  psdmvr  22236  cnprest  23351  txrest  23693  ptrescn  23701  flimrest  24045  txflf  24068  fclsrest  24086  tsmssubm  24205  mbfi1fseqlem4  25782  2sq2  27499  axcontlem7  29173  uhgreq12g  29268  nbuhgr2vtx1edgb  29555  wlkcomp  29833  uhgrwkspthlem2  29956  clwlkcomp  29981  wlknwwlksnbij  30090  hashecclwwlkn1  30281  umgrhashecclwwlk  30282  numclwwlk1lem2fo  30562  ubthlem1  31075  pjimai  32381  atcv1  32585  chirredi  32599  mplvrpmrhm  33846  bj-restsn  37577  fvineqsneu  37910  pibt2  37916  wl-sbcom2d-lem1  38067  wl-sbalnae  38070  ptrest  38123  poimirlem28  38152  heicant  38159  ftc1anclem1  38197  sbeqi  38663  ralbi12f  38664  iineq12f  38668  brcnvepres  38776  elrnressn  38784  qmapeldisjsim  39364  tfsconcat0i  43927  nzss  44898  sinnpoly  47490  or2expropbilem1  47631  modmkpkne  47966  ich2exprop  48082  ichnreuop  48083  ichreuopeq  48084  reuopreuprim  48137  rngcinvALTV  48903  snlindsntorlem  49097  itscnhlc0xyqsol  49392  opndisj  49529