Theorem sylan9bbr 733

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383

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

This theorem is referenced by:  pm5.75  974  pm5.75OLD  975  sbcom2  2433  sbal1  2448  sbal2  2449  mpteq12f  4661  otthg  4880  fmptsng  6339  f1oiso  6501  mpt2eq123  6612  elovmpt2rab  6778  elovmpt2rab1  6779  ovmpt3rabdm  6790  elovmpt3rab1  6791  tfindsg  6952  findsg  6985  dfoprab4f  7117  opiota  7118  fmpt2x  7125  oalimcl  7527  oeeui  7569  nnmword  7600  isinf  8058  elfi  8202  brwdomn0  8357  alephval3  8816  dfac2  8836  fin17  9099  isfin7-2  9101  ltmpi  9605  addclprlem1  9717  distrlem4pr  9727  1idpr  9730  qreccl  11684  0fz1  12232  zmodid2  12560  ccatrcl1  13229  eqwrds3  13552  divgcdcoprm0  15217  sscntz  17582  gexdvds  17822  cnprest  20903  txrest  21244  ptrescn  21252  flimrest  21597  txflf  21620  fclsrest  21638  tsmssubm  21756  mbfi1fseqlem4  23291  axcontlem7  25650  uhgreq12g  25731  hashecclwwlkn1  26361  usghashecclwwlk  26362  numclwlk1lem2fo  26622  ubthlem1  27110  pjimai  28419  atcv1  28623  chirredi  28637  bj-restsn  32216  wl-sbcom2d-lem1  32521  wl-sbalnae  32524  ptrest  32578  poimirlem28  32607  heicant  32614  ftc1anclem1  32655  sbeqi  33138  ralbi12f  33139  iineq12f  33143  nzss  37538  raaan2  39824  nbuhgr2vtx1edgb  40574  1wlkcomp  40835  uhgr1wlkspthlem2  40960  clWlkcomp  40986  hashecclwwlksn1  41261  umgrhashecclwwlk  41262  av-numclwlk1lem2fo  41525  rngcinv  41773  rngcinvALTV  41785  ringcinv  41824  ringcinvALTV  41848  snlindsntorlem  42053