Theorem sylan9bbr 737

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ 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 197  df-an 385

This theorem is referenced by:  pm5.75  998  sbcom2  2473  sbal1  2488  sbal2  2489  mpteq12f  4764  otthg  4983  fmptsng  6475  f1oiso  6641  mpt2eq123  6756  elovmpt2rab  6922  elovmpt2rab1  6923  ovmpt3rabdm  6934  elovmpt3rab1  6935  tfindsg  7102  findsg  7135  dfoprab4f  7270  opiota  7273  fmpt2x  7281  oalimcl  7685  oeeui  7727  nnmword  7758  isinf  8214  elfi  8360  brwdomn0  8515  alephval3  8971  dfac2  8991  fin17  9254  isfin7-2  9256  ltmpi  9764  addclprlem1  9876  distrlem4pr  9886  1idpr  9889  qreccl  11846  0fz1  12399  zmodid2  12738  ccatrcl1  13412  eqwrds3  13750  divgcdcoprm0  15426  sscntz  17805  gexdvds  18045  cnprest  21141  txrest  21482  ptrescn  21490  flimrest  21834  txflf  21857  fclsrest  21875  tsmssubm  21993  mbfi1fseqlem4  23530  axcontlem7  25895  uhgreq12g  26005  nbuhgr2vtx1edgb  26293  wlkcomp  26582  uhgrwkspthlem2  26706  clwlkcomp  26731  hashecclwwlkn1  27041  umgrhashecclwwlk  27042  numclwlk1lem2fo  27348  ubthlem1  27854  pjimai  29163  atcv1  29367  chirredi  29381  bj-restsn  33160  wl-sbcom2d-lem1  33472  wl-sbalnae  33475  ptrest  33538  poimirlem28  33567  heicant  33574  ftc1anclem1  33615  sbeqi  34098  ralbi12f  34099  iineq12f  34103  brcnvepres  34174  nzss  38833  raaan2  41496  rngcinv  42306  rngcinvALTV  42318  ringcinv  42357  ringcinvALTV  42381  snlindsntorlem  42584