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  2174  sbal1  2526  sbal2  2527  raaan2  4484  mpteq12f  5192  otthg  5445  fmptsng  7142  f1oiso  7326  mpoeq123  7461  elovmporab  7635  elovmporab1w  7636  elovmporab1  7637  ovmpt3rabdm  7648  elovmpt3rab1  7649  tfindsg  7837  findsg  7873  dfoprab4f  8035  opiota  8038  fmpox  8046  oalimcl  8524  oeeui  8566  nnmword  8597  isinf  9207  isinfOLD  9208  elfi  9364  brwdomn0  9522  alephval3  10063  dfac2b  10084  fin17  10347  isfin7-2  10349  ltmpi  10857  addclprlem1  10969  distrlem4pr  10979  1idpr  10982  qreccl  12928  0fz1  13505  zmodid2  13861  ccatrcl1  14559  eqwrds3  14927  divgcdcoprm0  16635  sscntz  19258  gexdvds  19514  rngcinv  20546  psdmvr  22056  cnprest  23176  txrest  23518  ptrescn  23526  flimrest  23870  txflf  23893  fclsrest  23911  tsmssubm  24030  mbfi1fseqlem4  25619  2sq2  27344  axcontlem7  28897  uhgreq12g  28992  nbuhgr2vtx1edgb  29279  wlkcomp  29559  uhgrwkspthlem2  29684  clwlkcomp  29709  wlknwwlksnbij  29818  hashecclwwlkn1  30006  umgrhashecclwwlk  30007  numclwwlk1lem2fo  30287  ubthlem1  30799  pjimai  32105  atcv1  32309  chirredi  32323  bj-restsn  37070  fvineqsneu  37399  pibt2  37405  wl-sbcom2d-lem1  37547  wl-sbalnae  37550  ptrest  37613  poimirlem28  37642  heicant  37649  ftc1anclem1  37687  sbeqi  38153  ralbi12f  38154  iineq12f  38158  brcnvepres  38256  elrnressn  38262  tfsconcat0i  43334  nzss  44306  sinnpoly  46892  or2expropbilem1  47033  modmkpkne  47362  ich2exprop  47472  ichnreuop  47473  ichreuopeq  47474  reuopreuprim  47527  rngcinvALTV  48264  snlindsntorlem  48459  itscnhlc0xyqsol  48754  opndisj  48891