Theorem sylan9bb 514

Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)

Hypotheses

Ref	Expression
sylan9bb.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
sylan9bb.2	⊢ (𝜃 → (𝜒 ↔ 𝜏))

Assertion

Ref	Expression
sylan9bb	⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏))

Proof of Theorem sylan9bb

Step	Hyp	Ref	Expression
1		sylan9bb.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	adantr 481	. 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜒))
3		sylan9bb.2	. . 3 ⊢ (𝜃 → (𝜒 ↔ 𝜏))
4	3	adantl 482	. 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜒 ↔ 𝜏))
5	2, 4	bitrd 280	1 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  sylan9bbr  515  baibd  544  syl3an9b  1442  nanbi12  1510  elequ12  2137  sbcom2  2183  2sb5rf  2480  2sb6rf  2481  eqeqan12d  2753  eleq12  2829  ceqsrex2v  3596  elabd2  3608  elabgt  3610  sseq12  3942  csbie2df  4372  2ralsng  4611  rexprgf  4628  rextpg  4632  breq12  5078  reusv2lem5  5332  opelopabg  5481  brabg  5482  opelopabgf  5483  opelopab2  5484  rbropapd  5505  poeq12d  5532  soeq12d  5550  freq12d  5588  seeq12d  5591  weeq12d  5608  ralxpf  5789  feq23  6637  f00  6710  fconstg  6715  f1oeq23  6759  f1o00  6803  fnelfp  7120  fnelnfp  7122  isofrlem  7285  f1oiso  7296  riota1a  7336  cbvmpox  7450  caovord  7568  caovord3  7570  f1oweALT  7915  mpof1o2d  8066  oaordex  8484  oaass  8487  odi  8505  findcard2s  9091  unfilem1  9206  tfsnfin2  9264  suppeqfsuppbi  9283  oieu  9445  r1pw  9761  carddomi2  9886  isacn  9958  djudom2  10098  axdc2  10363  alephval2  10487  distrlem4pr  10941  axpre-sup  11084  nn0ind-raph  12621  elpq  12917  xnn0xadd0  13191  elfz  13459  elfzp12  13549  expeq0  14046  leiso  14413  wrd2ind  14677  trcleq12lem  14947  dfrtrclrec2  15012  shftfib  15026  absdvdsb  16235  dvdsabsb  16236  dvdsabseq  16274  unbenlem  16871  isprs  18254  isdrs  18259  pltval  18288  lublecllem  18316  istos  18374  isdlat  18480  znfld  21536  tgss2  22971  isopn2  23016  cnpf2  23234  lmbr  23242  isreg2  23361  fclsrest  24008  qustgplem  24105  ustuqtoplem  24223  xmetec  24418  nmogelb  24700  metdstri  24836  tcphcph  25223  ulmval  26364  2lgslem1a  27373  elmade  27868  bdayle  27927  iscgrg  28599  istrlson  29792  ispthson  29829  isspthson  29830  elwwlks2on  30048  eupth2lem1  30307  eigrei  31924  eigorthi  31927  jplem1  32358  superpos  32444  chrelati  32454  br8d  32701  ellpi  33457  issiga  34305  eulerpartlemgvv  34569  cplgredgex  35358  acycgrcycl  35384  br8  35993  br6  35994  br4  35995  brsegle  36345  topfne  36591  tailfb  36614  filnetlem1  36615  nndivsub  36694  bj-rest10  37455  isbasisrelowllem1  37726  isbasisrelowllem2  37727  fvineqsnf1  37781  wl-2sb6d  37938  curf  37974  curunc  37978  poimirlem26  38022  mblfinlem2  38034  cnambfre  38044  itgaddnclem2  38055  ftc1anclem1  38069  grpokerinj  38269  rngoisoval  38353  smprngopr  38428  parteq12  39255  ax12eq  39442  ax12el  39443  2llnjN  40068  2lplnj  40121  elpadd0  40310  lauteq  40596  lpolconN  41988  rexrabdioph  43248  tfsnfin  43806  eliunov2  44132  nzss  44770  iotasbc2  44873  or2expropbilem2  47504  elsetpreimafvbi  47874  reuopreuprim  48009  grlicref  48511  cbvmpox2  48835  naryfvalel  49129  line2x  49253  brab2ddw  49327  brab2ddw2  49328