Theorem sylan9bbr 513

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

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

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 399

This theorem is referenced by:  bimsc1  840  pm5.75  1025  sbcom2  2163  sbal1  2568  sbal2  2569  sbal2OLD  2570  raaan2  4464  mpteq12f  5142  otthg  5370  fmptsng  6925  f1oiso  7098  mpoeq123  7220  elovmporab  7385  elovmporab1w  7386  elovmporab1  7387  ovmpt3rabdm  7398  elovmpt3rab1  7399  tfindsg  7569  findsg  7603  dfoprab4f  7748  opiota  7751  fmpox  7759  oalimcl  8180  oeeui  8222  nnmword  8253  isinf  8725  elfi  8871  brwdomn0  9027  alephval3  9530  dfac2b  9550  fin17  9810  isfin7-2  9812  ltmpi  10320  addclprlem1  10432  distrlem4pr  10442  1idpr  10445  qreccl  12362  0fz1  12921  zmodid2  13261  ccatrcl1  13942  eqwrds3  14319  divgcdcoprm0  16003  sscntz  18450  gexdvds  18703  cnprest  21891  txrest  22233  ptrescn  22241  flimrest  22585  txflf  22608  fclsrest  22626  tsmssubm  22745  mbfi1fseqlem4  24313  2sq2  26003  axcontlem7  26750  uhgreq12g  26844  nbuhgr2vtx1edgb  27128  wlkcomp  27406  uhgrwkspthlem2  27529  clwlkcomp  27554  wlknwwlksnbij  27660  hashecclwwlkn1  27850  umgrhashecclwwlk  27851  numclwwlk1lem2fo  28131  ubthlem1  28641  pjimai  29947  atcv1  30151  chirredi  30165  bj-restsn  34367  fvineqsneu  34686  pibt2  34692  wl-sbcom2d-lem1  34789  wl-sbalnae  34792  ptrest  34885  poimirlem28  34914  heicant  34921  ftc1anclem1  34961  sbeqi  35431  ralbi12f  35432  iineq12f  35436  brcnvepres  35522  nzss  40642  or2expropbilem1  43260  ich2exprop  43626  ichnreuop  43627  ichreuopeq  43628  reuopreuprim  43681  rngcinv  44245  rngcinvALTV  44257  ringcinv  44296  ringcinvALTV  44320  snlindsntorlem  44518  itscnhlc0xyqsol  44745