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  1434  nanbi12  1500  elequ12  2126  sbcom2  2174  2sb5rf  2480  2sb6rf  2481  eqeqan12d  2754  eqeq12OLD  2759  eleq12  2834  sbhypfOLD  3557  ceqsrex2v  3671  elabd2  3683  sseq12  4036  csbie2df  4466  2ralsng  4700  rexprgf  4718  rextpg  4724  breq12  5171  reusv2lem5  5420  opelopabg  5557  brabg  5558  opelopabgf  5559  opelopab2  5560  rbropapd  5583  poeq12d  5612  soeq12d  5631  freq12d  5669  seeq12d  5672  weeq12d  5689  ralxpf  5871  feq23  6731  f00  6803  fconstg  6808  f1oeq23  6853  f1o00  6897  fnelfp  7209  fnelnfp  7211  isofrlem  7376  f1oiso  7387  riota1a  7427  cbvmpox  7543  caovord  7661  caovord3  7663  f1oweALT  8013  oaordex  8614  oaass  8617  odi  8635  findcard2s  9231  unfilem1  9371  suppeqfsuppbi  9448  oieu  9608  r1pw  9914  carddomi2  10039  isacn  10113  djudom2  10253  axdc2  10518  alephval2  10641  distrlem4pr  11095  axpre-sup  11238  nn0ind-raph  12743  elpq  13040  xnn0xadd0  13309  elfz  13573  elfzp12  13663  expeq0  14143  leiso  14508  wrd2ind  14771  trcleq12lem  15042  dfrtrclrec2  15107  shftfib  15121  absdvdsb  16323  dvdsabsb  16324  dvdsabseq  16361  unbenlem  16955  isprs  18367  isdrs  18371  pltval  18402  lublecllem  18430  istos  18488  isdlat  18592  znfld  21602  tgss2  23015  isopn2  23061  cnpf2  23279  lmbr  23287  isreg2  23406  fclsrest  24053  qustgplem  24150  ustuqtoplem  24269  xmetec  24465  nmogelb  24758  metdstri  24892  tcphcph  25290  ulmval  26441  2lgslem1a  27453  elmade  27924  iscgrg  28538  istrlson  29743  ispthson  29778  isspthson  29779  elwwlks2on  29992  eupth2lem1  30250  eigrei  31866  eigorthi  31869  jplem1  32300  superpos  32386  chrelati  32396  bian1d  32484  br8d  32632  ellpi  33366  issiga  34076  eulerpartlemgvv  34341  cplgredgex  35088  acycgrcycl  35115  br8  35718  br6  35719  br4  35720  brsegle  36072  topfne  36320  tailfb  36343  filnetlem1  36344  nndivsub  36423  bj-rest10  37054  isbasisrelowllem1  37321  isbasisrelowllem2  37322  fvineqsnf1  37376  wl-2sb6d  37512  curf  37558  curunc  37562  poimirlem26  37606  mblfinlem2  37618  cnambfre  37628  itgaddnclem2  37639  ftc1anclem1  37653  grpokerinj  37853  rngoisoval  37937  smprngopr  38012  parteq12  38732  ax12eq  38897  ax12el  38898  2llnjN  39524  2lplnj  39577  elpadd0  39766  lauteq  40052  lpolconN  41444  f1o2d2  42228  rexrabdioph  42750  tfsnfin  43314  eliunov2  43641  nzss  44286  iotasbc2  44389  or2expropbilem2  46948  elsetpreimafvbi  47265  reuopreuprim  47400  grlicref  47829  cbvmpox2  48060  naryfvalel  48364  line2x  48488