Theorem sylan9bb 510

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 278	1 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 397

This theorem is referenced by:  sylan9bbr  511  baibd  540  syl3an9b  1434  nanbi12  1501  sbcom2  2161  2sb5rf  2470  2sb6rf  2471  eqeqan12d  2745  eqeq12OLD  2750  eleq12  2822  sbhypfOLD  3536  ceqsrex2v  3642  elabd2  3656  sseq12  4005  csbie2df  4436  2ralsng  4673  rexprgf  4690  rextpg  4696  breq12  5146  reusv2lem5  5393  opelopabg  5531  brabg  5532  opelopabgf  5533  opelopab2  5534  rbropapd  5557  ralxpf  5838  feq23  6688  f00  6760  fconstg  6765  f1oeq23  6811  f1o00  6855  fnelfp  7157  fnelnfp  7159  isofrlem  7321  f1oiso  7332  riota1a  7372  cbvmpox  7486  caovord  7601  caovord3  7603  f1oweALT  7941  oaordex  8541  oaass  8544  odi  8562  findcard2s  9148  unfilem1  9293  suppeqfsuppbi  9360  oieu  9516  r1pw  9822  carddomi2  9947  isacn  10021  djudom2  10160  axdc2  10426  alephval2  10549  fpwwe2cbv  10607  fpwwe2lem2  10609  fpwwecbv  10621  fpwwelem  10622  canthwelem  10627  canthwe  10628  distrlem4pr  11003  axpre-sup  11146  nn0ind-raph  12644  elpq  12941  xnn0xadd0  13208  elfz  13472  elfzp12  13562  expeq0  14040  leiso  14402  wrd2ind  14655  trcleq12lem  14922  dfrtrclrec2  14987  shftfib  15001  absdvdsb  16200  dvdsabsb  16201  dvdsabseq  16238  unbenlem  16823  isprs  18232  isdrs  18236  pltval  18267  lublecllem  18295  istos  18353  isdlat  18457  znfld  21049  tgss2  22419  isopn2  22465  cnpf2  22683  lmbr  22691  isreg2  22810  fclsrest  23457  qustgplem  23554  ustuqtoplem  23673  xmetec  23869  nmogelb  24162  metdstri  24296  tcphcph  24683  ulmval  25821  2lgslem1a  26821  elmade  27285  iscgrg  27628  istrlson  28829  ispthson  28864  isspthson  28865  elwwlks2on  29078  eupth2lem1  29336  eigrei  30950  eigorthi  30953  jplem1  31384  superpos  31470  chrelati  31480  br8d  31707  issiga  32939  eulerpartlemgvv  33204  cplgredgex  33940  acycgrcycl  33967  br8  34554  br6  34555  br4  34556  brsegle  34908  topfne  35041  tailfb  35064  filnetlem1  35065  nndivsub  35144  bj-elequ12  35358  bj-rest10  35771  isbasisrelowllem1  36038  isbasisrelowllem2  36039  fvineqsnf1  36093  wl-2sb6d  36225  curf  36268  curunc  36272  poimirlem26  36316  mblfinlem2  36328  cnambfre  36338  itgaddnclem2  36349  ftc1anclem1  36363  grpokerinj  36564  rngoisoval  36648  smprngopr  36723  parteq12  37449  ax12eq  37614  ax12el  37615  2llnjN  38241  2lplnj  38294  elpadd0  38483  lauteq  38769  lpolconN  40161  rexrabdioph  41301  tfsnfin  41871  eliunov2  42199  nzss  42845  iotasbc2  42948  or2expropbilem2  45513  elsetpreimafvbi  45829  reuopreuprim  45964  cbvmpox2  46657  naryfvalel  46962  line2x  47086