Theorem sylan9bbr 510

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  bimsc1  845  pm5.75  1031  sbcom2  2179  sbal1  2533  sbal2  2534  raaan2  4476  mpteq12f  5184  otthg  5434  dm0rn0  5874  fmptsng  7116  f1oiso  7299  mpoeq123  7432  elovmporab  7606  elovmporab1w  7607  elovmporab1  7608  ovmpt3rabdm  7619  elovmpt3rab1  7620  tfindsg  7805  findsg  7841  dfoprab4f  8002  opiota  8005  fmpox  8013  oalimcl  8489  oeeui  8532  nnmword  8563  isinf  9169  elfi  9320  brwdomn0  9478  alephval3  10024  dfac2b  10045  fin17  10308  isfin7-2  10310  ltmpi  10819  addclprlem1  10931  distrlem4pr  10941  1idpr  10944  qreccl  12886  0fz1  13464  zmodid2  13823  ccatrcl1  14522  eqwrds3  14888  divgcdcoprm0  16596  sscntz  19259  gexdvds  19517  rngcinv  20574  psdmvr  22116  cnprest  23237  txrest  23579  ptrescn  23587  flimrest  23931  txflf  23954  fclsrest  23972  tsmssubm  24091  mbfi1fseqlem4  25679  2sq2  27404  axcontlem7  29047  uhgreq12g  29142  nbuhgr2vtx1edgb  29429  wlkcomp  29708  uhgrwkspthlem2  29831  clwlkcomp  29856  wlknwwlksnbij  29965  hashecclwwlkn1  30156  umgrhashecclwwlk  30157  numclwwlk1lem2fo  30437  ubthlem1  30949  pjimai  32255  atcv1  32459  chirredi  32473  mplvrpmrhm  33714  bj-restsn  37289  fvineqsneu  37618  pibt2  37624  wl-sbcom2d-lem1  37766  wl-sbalnae  37769  ptrest  37822  poimirlem28  37851  heicant  37858  ftc1anclem1  37896  sbeqi  38362  ralbi12f  38363  iineq12f  38367  brcnvepres  38475  elrnressn  38483  qmapeldisjsim  39063  tfsconcat0i  43654  nzss  44625  sinnpoly  47204  or2expropbilem1  47345  modmkpkne  47674  ich2exprop  47784  ichnreuop  47785  ichreuopeq  47786  reuopreuprim  47839  rngcinvALTV  48589  snlindsntorlem  48783  itscnhlc0xyqsol  49078  opndisj  49215