Theorem sylan9bb 509

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 480	. 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜒))
3		sylan9bb.2	. . 3 ⊢ (𝜃 → (𝜒 ↔ 𝜏))
4	3	adantl 481	. 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜒 ↔ 𝜏))
5	2, 4	bitrd 279	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:  sylan9bbr  510  baibd  539  syl3an9b  1435  nanbi12  1502  elequ12  2125  sbcom2  2172  2sb5rf  2476  2sb6rf  2477  eqeqan12d  2750  eqeq12OLD  2755  eleq12  2830  sbhypfOLD  3544  ceqsrex2v  3657  elabd2  3669  sseq12  4010  csbie2df  4442  2ralsng  4677  rexprgf  4694  rextpg  4698  breq12  5147  reusv2lem5  5401  opelopabg  5542  brabg  5543  opelopabgf  5544  opelopab2  5545  rbropapd  5568  poeq12d  5596  soeq12d  5614  freq12d  5653  seeq12d  5656  weeq12d  5673  ralxpf  5856  feq23  6718  f00  6789  fconstg  6794  f1oeq23  6838  f1o00  6882  fnelfp  7196  fnelnfp  7198  isofrlem  7361  f1oiso  7372  riota1a  7411  cbvmpox  7527  caovord  7645  caovord3  7647  f1oweALT  7998  oaordex  8597  oaass  8600  odi  8618  findcard2s  9206  unfilem1  9344  suppeqfsuppbi  9420  oieu  9580  r1pw  9886  carddomi2  10011  isacn  10085  djudom2  10225  axdc2  10490  alephval2  10613  distrlem4pr  11067  axpre-sup  11210  nn0ind-raph  12720  elpq  13018  xnn0xadd0  13290  elfz  13554  elfzp12  13644  expeq0  14134  leiso  14499  wrd2ind  14762  trcleq12lem  15033  dfrtrclrec2  15098  shftfib  15112  absdvdsb  16313  dvdsabsb  16314  dvdsabseq  16351  unbenlem  16947  isprs  18343  isdrs  18348  pltval  18378  lublecllem  18406  istos  18464  isdlat  18568  znfld  21580  tgss2  22995  isopn2  23041  cnpf2  23259  lmbr  23267  isreg2  23386  fclsrest  24033  qustgplem  24130  ustuqtoplem  24249  xmetec  24445  nmogelb  24738  metdstri  24874  tcphcph  25272  ulmval  26424  2lgslem1a  27436  elmade  27907  iscgrg  28521  istrlson  29726  ispthson  29763  isspthson  29764  elwwlks2on  29980  eupth2lem1  30238  eigrei  31854  eigorthi  31857  jplem1  32288  superpos  32374  chrelati  32384  bian1d  32476  br8d  32623  ellpi  33402  issiga  34114  eulerpartlemgvv  34379  cplgredgex  35127  acycgrcycl  35153  br8  35757  br6  35758  br4  35759  brsegle  36110  topfne  36356  tailfb  36379  filnetlem1  36380  nndivsub  36459  bj-rest10  37090  isbasisrelowllem1  37357  isbasisrelowllem2  37358  fvineqsnf1  37412  wl-2sb6d  37560  curf  37606  curunc  37610  poimirlem26  37654  mblfinlem2  37666  cnambfre  37676  itgaddnclem2  37687  ftc1anclem1  37701  grpokerinj  37901  rngoisoval  37985  smprngopr  38060  parteq12  38778  ax12eq  38943  ax12el  38944  2llnjN  39570  2lplnj  39623  elpadd0  39812  lauteq  40098  lpolconN  41490  f1o2d2  42274  rexrabdioph  42810  tfsnfin  43370  eliunov2  43697  nzss  44341  iotasbc2  44444  or2expropbilem2  47050  elsetpreimafvbi  47383  reuopreuprim  47518  grlicref  47977  cbvmpox2  48257  naryfvalel  48556  line2x  48680  brab2ddw  48747  brab2ddw2  48748