Theorem sylan9bbr 520

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  bimsc1  858  pm5.75  1046  sbcom2  2208  sbal1  2557  sbal2  2558  raaan2  4477  mpteq12f  5189  otthg  5453  dm0rn0  5905  fmptsng  7173  f1oiso  7359  mpoeq123  7492  elovmporab  7667  elovmporab1w  7668  elovmporab1  7669  ovmpt3rabdm  7680  elovmpt3rab1  7681  tfindsg  7872  findsg  7909  dfoprab4f  8067  opiota  8070  fmpox  8078  oalimcl  8568  oeeui  8611  nnmword  8642  isinf  9256  elfi  9405  brwdomn0  9563  alephval3  10189  dfac2b  10209  fin17  10472  isfin7-2  10474  ltmpi  10989  addclprlem1  11101  distrlem4pr  11111  1idpr  11114  qreccl  13097  0fz1  13677  zmodid2  14039  ccatrcl1  14741  eqwrds3  15114  divgcdcoprm0  16840  sscntz  19540  gexdvds  19798  rngcinv  20889  psdmvr  22490  cnprest  23607  txrest  23950  ptrescn  23958  flimrest  24302  txflf  24325  fclsrest  24343  tsmssubm  24462  mbfi1fseqlem4  26039  2sq2  27760  axcontlem7  29548  uhgreq12g  29643  nbuhgr2vtx1edgb  29933  wlkcomp  30211  uhgrwkspthlem2  30340  clwlkcomp  30366  wlknwwlksnbij  30477  hashecclwwlkn1  30668  umgrhashecclwwlk  30669  numclwwlk1lem2fo  30959  ubthlem1  31472  pjimai  32778  atcv1  32982  chirredi  32996  mplvrpmrhm  34221  bj-restsn  38045  fvineqsneu  38377  pibt2  38383  wl-sbcom2d-lem1  38534  wl-sbalnae  38537  ptrest  38580  poimirlem28  38609  heicant  38616  ftc1anclem1  38654  sbeqi  39134  ralbi12f  39135  iineq12f  39139  brcnvepres  39247  elrnressn  39255  qmapeldisjsim  39835  tfsconcat0i  44389  nzss  45343  sinnpoly  47983  or2expropbilem1  48144  modmkpkne  48479  ich2exprop  48595  ichnreuop  48596  ichreuopeq  48597  reuopreuprim  48650  rngcinvALTV  49415  snlindsntorlem  49624  itscnhlc0xyqsol  49919  opndisj  50053