Theorem sylan9bbr 514

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  bimsc1  841  pm5.75  1026  sbcom2  2165  sbal1  2548  sbal2  2549  sbal2OLD  2550  raaan2  4422  mpteq12f  5113  otthg  5342  fmptsng  6907  f1oiso  7083  mpoeq123  7205  elovmporab  7371  elovmporab1w  7372  elovmporab1  7373  ovmpt3rabdm  7384  elovmpt3rab1  7385  tfindsg  7555  findsg  7590  dfoprab4f  7736  opiota  7739  fmpox  7747  oalimcl  8169  oeeui  8211  nnmword  8242  isinf  8715  elfi  8861  brwdomn0  9017  alephval3  9521  dfac2b  9541  fin17  9805  isfin7-2  9807  ltmpi  10315  addclprlem1  10427  distrlem4pr  10437  1idpr  10440  qreccl  12356  0fz1  12922  zmodid2  13262  ccatrcl1  13939  eqwrds3  14316  divgcdcoprm0  15999  sscntz  18448  gexdvds  18701  cnprest  21894  txrest  22236  ptrescn  22244  flimrest  22588  txflf  22611  fclsrest  22629  tsmssubm  22748  mbfi1fseqlem4  24322  2sq2  26017  axcontlem7  26764  uhgreq12g  26858  nbuhgr2vtx1edgb  27142  wlkcomp  27420  uhgrwkspthlem2  27543  clwlkcomp  27568  wlknwwlksnbij  27674  hashecclwwlkn1  27862  umgrhashecclwwlk  27863  numclwwlk1lem2fo  28143  ubthlem1  28653  pjimai  29959  atcv1  30163  chirredi  30177  bj-restsn  34497  fvineqsneu  34828  pibt2  34834  wl-sbcom2d-lem1  34960  wl-sbalnae  34963  ptrest  35056  poimirlem28  35085  heicant  35092  ftc1anclem1  35130  sbeqi  35597  ralbi12f  35598  iineq12f  35602  brcnvepres  35688  nzss  41021  or2expropbilem1  43624  ich2exprop  43988  ichnreuop  43989  ichreuopeq  43990  reuopreuprim  44043  rngcinv  44605  rngcinvALTV  44617  ringcinv  44656  ringcinvALTV  44680  snlindsntorlem  44879  itscnhlc0xyqsol  45179