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  843  pm5.75  1029  sbcom2  2174  sbal1  2536  sbal2  2537  raaan2  4544  mpteq12f  5254  otthg  5505  fmptsng  7202  f1oiso  7387  mpoeq123  7522  elovmporab  7696  elovmporab1w  7697  elovmporab1  7698  ovmpt3rabdm  7709  elovmpt3rab1  7710  tfindsg  7898  findsg  7937  dfoprab4f  8097  opiota  8100  fmpox  8108  oalimcl  8616  oeeui  8658  nnmword  8689  isinf  9323  isinfOLD  9324  elfi  9482  brwdomn0  9638  alephval3  10179  dfac2b  10200  fin17  10463  isfin7-2  10465  ltmpi  10973  addclprlem1  11085  distrlem4pr  11095  1idpr  11098  qreccl  13034  0fz1  13604  zmodid2  13950  ccatrcl1  14642  eqwrds3  15010  divgcdcoprm0  16712  sscntz  19366  gexdvds  19626  rngcinv  20659  cnprest  23318  txrest  23660  ptrescn  23668  flimrest  24012  txflf  24035  fclsrest  24053  tsmssubm  24172  mbfi1fseqlem4  25773  2sq2  27495  axcontlem7  29003  uhgreq12g  29100  nbuhgr2vtx1edgb  29387  wlkcomp  29667  uhgrwkspthlem2  29790  clwlkcomp  29815  wlknwwlksnbij  29921  hashecclwwlkn1  30109  umgrhashecclwwlk  30110  numclwwlk1lem2fo  30390  ubthlem1  30902  pjimai  32208  atcv1  32412  chirredi  32426  bj-restsn  37048  fvineqsneu  37377  pibt2  37383  wl-sbcom2d-lem1  37513  wl-sbalnae  37516  ptrest  37579  poimirlem28  37608  heicant  37615  ftc1anclem1  37653  sbeqi  38119  ralbi12f  38120  iineq12f  38124  brcnvepres  38223  elrnressn  38229  tfsconcat0i  43307  nzss  44286  or2expropbilem1  46947  ich2exprop  47345  ichnreuop  47346  ichreuopeq  47347  reuopreuprim  47400  rngcinvALTV  47999  snlindsntorlem  48199  itscnhlc0xyqsol  48499  opndisj  48582