Theorem sylan9bb 508

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 479	. 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜒))
3		sylan9bb.2	. . 3 ⊢ (𝜃 → (𝜒 ↔ 𝜏))
4	3	adantl 480	. 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜒 ↔ 𝜏))
5	2, 4	bitrd 278	1 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394

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 395

This theorem is referenced by:  sylan9bbr  509  baibd  538  syl3an9b  1430  nanbi12  1496  sbcom2  2162  2sb5rf  2465  2sb6rf  2466  eqeqan12d  2739  eqeq12OLD  2744  eleq12  2815  sbhypfOLD  3529  ceqsrex2v  3641  elabd2  3655  sseq12  4004  csbie2df  4442  2ralsng  4682  rexprgf  4699  rextpg  4705  breq12  5154  reusv2lem5  5402  opelopabg  5540  brabg  5541  opelopabgf  5542  opelopab2  5543  rbropapd  5566  ralxpf  5849  feq23  6707  f00  6779  fconstg  6784  f1oeq23  6829  f1o00  6873  fnelfp  7184  fnelnfp  7186  isofrlem  7347  f1oiso  7358  riota1a  7398  cbvmpox  7513  caovord  7632  caovord3  7634  f1oweALT  7977  oaordex  8579  oaass  8582  odi  8600  findcard2s  9190  unfilem1  9335  suppeqfsuppbi  9404  oieu  9564  r1pw  9870  carddomi2  9995  isacn  10069  djudom2  10208  axdc2  10474  alephval2  10597  fpwwe2cbv  10655  fpwwe2lem2  10657  fpwwecbv  10669  fpwwelem  10670  canthwelem  10675  canthwe  10676  distrlem4pr  11051  axpre-sup  11194  nn0ind-raph  12695  elpq  12992  xnn0xadd0  13261  elfz  13525  elfzp12  13615  expeq0  14093  leiso  14456  wrd2ind  14709  trcleq12lem  14976  dfrtrclrec2  15041  shftfib  15055  absdvdsb  16255  dvdsabsb  16256  dvdsabseq  16293  unbenlem  16880  isprs  18292  isdrs  18296  pltval  18327  lublecllem  18355  istos  18413  isdlat  18517  znfld  21511  tgss2  22934  isopn2  22980  cnpf2  23198  lmbr  23206  isreg2  23325  fclsrest  23972  qustgplem  24069  ustuqtoplem  24188  xmetec  24384  nmogelb  24677  metdstri  24811  tcphcph  25209  ulmval  26361  2lgslem1a  27369  elmade  27840  iscgrg  28388  istrlson  29593  ispthson  29628  isspthson  29629  elwwlks2on  29842  eupth2lem1  30100  eigrei  31716  eigorthi  31719  jplem1  32150  superpos  32236  chrelati  32246  br8d  32479  ellpi  33185  issiga  33862  eulerpartlemgvv  34127  cplgredgex  34861  acycgrcycl  34888  br8  35481  br6  35482  br4  35483  brsegle  35835  topfne  35969  tailfb  35992  filnetlem1  35993  nndivsub  36072  bj-elequ12  36286  bj-rest10  36698  isbasisrelowllem1  36965  isbasisrelowllem2  36966  fvineqsnf1  37020  wl-2sb6d  37156  curf  37202  curunc  37206  poimirlem26  37250  mblfinlem2  37262  cnambfre  37272  itgaddnclem2  37283  ftc1anclem1  37297  grpokerinj  37497  rngoisoval  37581  smprngopr  37656  parteq12  38378  ax12eq  38543  ax12el  38544  2llnjN  39170  2lplnj  39223  elpadd0  39412  lauteq  39698  lpolconN  41090  f1o2d2  41857  rexrabdioph  42356  tfsnfin  42923  eliunov2  43251  nzss  43896  iotasbc2  43999  or2expropbilem2  46553  elsetpreimafvbi  46868  reuopreuprim  47003  cbvmpox2  47585  naryfvalel  47889  line2x  48013