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  2178  sbal1  2530  sbal2  2531  raaan2  4473  mpteq12f  5181  otthg  5431  dm0rn0  5871  fmptsng  7112  f1oiso  7295  mpoeq123  7428  elovmporab  7602  elovmporab1w  7603  elovmporab1  7604  ovmpt3rabdm  7615  elovmpt3rab1  7616  tfindsg  7801  findsg  7837  dfoprab4f  7998  opiota  8001  fmpox  8009  oalimcl  8485  oeeui  8528  nnmword  8559  isinf  9163  elfi  9314  brwdomn0  9472  alephval3  10018  dfac2b  10039  fin17  10302  isfin7-2  10304  ltmpi  10813  addclprlem1  10925  distrlem4pr  10935  1idpr  10938  qreccl  12880  0fz1  13458  zmodid2  13817  ccatrcl1  14516  eqwrds3  14882  divgcdcoprm0  16590  sscntz  19253  gexdvds  19511  rngcinv  20568  psdmvr  22110  cnprest  23231  txrest  23573  ptrescn  23581  flimrest  23925  txflf  23948  fclsrest  23966  tsmssubm  24085  mbfi1fseqlem4  25673  2sq2  27398  axcontlem7  28992  uhgreq12g  29087  nbuhgr2vtx1edgb  29374  wlkcomp  29653  uhgrwkspthlem2  29776  clwlkcomp  29801  wlknwwlksnbij  29910  hashecclwwlkn1  30101  umgrhashecclwwlk  30102  numclwwlk1lem2fo  30382  ubthlem1  30894  pjimai  32200  atcv1  32404  chirredi  32418  mplvrpmrhm  33661  bj-restsn  37226  fvineqsneu  37555  pibt2  37561  wl-sbcom2d-lem1  37703  wl-sbalnae  37706  ptrest  37759  poimirlem28  37788  heicant  37795  ftc1anclem1  37833  sbeqi  38299  ralbi12f  38300  iineq12f  38304  brcnvepres  38404  elrnressn  38412  tfsconcat0i  43529  nzss  44500  sinnpoly  47079  or2expropbilem1  47220  modmkpkne  47549  ich2exprop  47659  ichnreuop  47660  ichreuopeq  47661  reuopreuprim  47714  rngcinvALTV  48464  snlindsntorlem  48658  itscnhlc0xyqsol  48953  opndisj  49090