Theorem sylan9bbr 509

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  bimsc1  840  pm5.75  1025  sbcom2  2159  sbal1  2525  sbal2  2526  raaan2  4523  mpteq12f  5235  otthg  5484  fmptsng  7167  f1oiso  7350  mpoeq123  7483  elovmporab  7654  elovmporab1w  7655  elovmporab1  7656  ovmpt3rabdm  7667  elovmpt3rab1  7668  tfindsg  7852  findsg  7892  dfoprab4f  8044  opiota  8047  fmpox  8055  oalimcl  8562  oeeui  8604  nnmword  8635  isinf  9262  isinfOLD  9263  elfi  9410  brwdomn0  9566  alephval3  10107  dfac2b  10127  fin17  10391  isfin7-2  10393  ltmpi  10901  addclprlem1  11013  distrlem4pr  11023  1idpr  11026  qreccl  12957  0fz1  13525  zmodid2  13868  ccatrcl1  14548  eqwrds3  14916  divgcdcoprm0  16606  sscntz  19231  gexdvds  19493  cnprest  23013  txrest  23355  ptrescn  23363  flimrest  23707  txflf  23730  fclsrest  23748  tsmssubm  23867  mbfi1fseqlem4  25468  2sq2  27172  axcontlem7  28495  uhgreq12g  28592  nbuhgr2vtx1edgb  28876  wlkcomp  29155  uhgrwkspthlem2  29278  clwlkcomp  29303  wlknwwlksnbij  29409  hashecclwwlkn1  29597  umgrhashecclwwlk  29598  numclwwlk1lem2fo  29878  ubthlem1  30390  pjimai  31696  atcv1  31900  chirredi  31914  bj-restsn  36266  fvineqsneu  36595  pibt2  36601  wl-sbcom2d-lem1  36727  wl-sbalnae  36730  ptrest  36790  poimirlem28  36819  heicant  36826  ftc1anclem1  36864  sbeqi  37330  ralbi12f  37331  iineq12f  37335  brcnvepres  37438  elrnressn  37444  tfsconcat0i  42397  nzss  43378  or2expropbilem1  46040  ich2exprop  46437  ichnreuop  46438  ichreuopeq  46439  reuopreuprim  46492  rngcinv  46967  rngcinvALTV  46979  snlindsntorlem  47238  itscnhlc0xyqsol  47538  opndisj  47622