Theorem sylan9bbr 506

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

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384

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 198  df-an 385

This theorem is referenced by:  pm5.75  1053  sbcom2  2537  sbal1  2552  sbal2  2553  mpteq12f  4892  otthg  5111  fmptsng  6631  f1oiso  6797  mpt2eq123  6916  elovmpt2rab  7082  elovmpt2rab1  7083  ovmpt3rabdm  7094  elovmpt3rab1  7095  tfindsg  7262  findsg  7295  dfoprab4f  7430  opiota  7433  fmpt2x  7441  oalimcl  7849  oeeui  7891  nnmword  7922  isinf  8384  elfi  8530  brwdomn0  8685  alephval3  9188  dfac2b  9208  dfac2OLD  9210  fin17  9473  isfin7-2  9475  ltmpi  9983  addclprlem1  10095  distrlem4pr  10105  1idpr  10108  qreccl  12014  0fz1  12573  zmodid2  12911  ccatrcl1  13571  eqwrds3  14005  divgcdcoprm0  15673  sscntz  18036  gexdvds  18277  cnprest  21387  txrest  21728  ptrescn  21736  flimrest  22080  txflf  22103  fclsrest  22121  tsmssubm  22239  mbfi1fseqlem4  23790  axcontlem7  26155  uhgreq12g  26251  nbuhgr2vtx1edgb  26541  wlkcomp  26831  uhgrwkspthlem2  26960  clwlkcomp  26985  wlknwwlksnbij  27102  hashecclwwlkn1  27347  umgrhashecclwwlk  27348  numclwwlk1lem2fo  27671  numclwwlk1lem2foOLD  27676  ubthlem1  28203  pjimai  29512  atcv1  29716  chirredi  29730  bj-restsn  33484  wl-sbcom2d-lem1  33788  wl-sbalnae  33791  ptrest  33853  poimirlem28  33882  heicant  33889  ftc1anclem1  33929  sbeqi  34410  ralbi12f  34411  iineq12f  34415  brcnvepres  34487  nzss  39214  raaan2  41831  rngcinv  42674  rngcinvALTV  42686  ringcinv  42725  ringcinvALTV  42749  snlindsntorlem  42952