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  2209  sbal1  2557  sbal2  2558  raaan2  4478  mpteq12f  5190  otthg  5461  dm0rn0  5910  fmptsng  7169  f1oiso  7355  mpoeq123  7488  elovmporab  7663  elovmporab1w  7664  elovmporab1  7665  ovmpt3rabdm  7676  elovmpt3rab1  7677  tfindsg  7863  findsg  7900  dfoprab4f  8058  opiota  8061  fmpox  8069  oalimcl  8554  oeeui  8597  nnmword  8628  isinf  9242  elfi  9390  brwdomn0  9548  alephval3  10138  dfac2b  10158  fin17  10421  isfin7-2  10423  ltmpi  10938  addclprlem1  11050  distrlem4pr  11060  1idpr  11063  qreccl  13044  0fz1  13623  zmodid2  13985  ccatrcl1  14686  eqwrds3  15059  divgcdcoprm0  16780  sscntz  19479  gexdvds  19737  rngcinv  20828  psdmvr  22429  cnprest  23546  txrest  23889  ptrescn  23897  flimrest  24241  txflf  24264  fclsrest  24282  tsmssubm  24401  mbfi1fseqlem4  25978  2sq2  27701  axcontlem7  29459  uhgreq12g  29554  nbuhgr2vtx1edgb  29844  wlkcomp  30122  uhgrwkspthlem2  30251  clwlkcomp  30277  wlknwwlksnbij  30388  hashecclwwlkn1  30579  umgrhashecclwwlk  30580  numclwwlk1lem2fo  30870  ubthlem1  31383  pjimai  32689  atcv1  32893  chirredi  32907  mplvrpmrhm  34090  bj-restsn  37899  fvineqsneu  38230  pibt2  38236  wl-sbcom2d-lem1  38387  wl-sbalnae  38390  ptrest  38433  poimirlem28  38462  heicant  38469  ftc1anclem1  38507  sbeqi  38972  ralbi12f  38973  iineq12f  38977  brcnvepres  39085  elrnressn  39093  qmapeldisjsim  39673  tfsconcat0i  44251  nzss  45206  sinnpoly  47824  or2expropbilem1  47985  modmkpkne  48320  ich2exprop  48436  ichnreuop  48437  ichreuopeq  48438  reuopreuprim  48491  rngcinvALTV  49256  snlindsntorlem  49465  itscnhlc0xyqsol  49760  opndisj  49894