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  1433  nanbi12  1500  elequ12  2124  sbcom2  2171  2sb5rf  2475  2sb6rf  2476  eqeqan12d  2749  eqeq12OLD  2754  eleq12  2829  sbhypfOLD  3545  ceqsrex2v  3658  elabd2  3670  sseq12  4023  csbie2df  4449  2ralsng  4683  rexprgf  4700  rextpg  4704  breq12  5153  reusv2lem5  5408  opelopabg  5548  brabg  5549  opelopabgf  5550  opelopab2  5551  rbropapd  5574  poeq12d  5602  soeq12d  5620  freq12d  5658  seeq12d  5661  weeq12d  5678  ralxpf  5860  feq23  6720  f00  6791  fconstg  6796  f1oeq23  6840  f1o00  6884  fnelfp  7195  fnelnfp  7197  isofrlem  7360  f1oiso  7371  riota1a  7410  cbvmpox  7526  caovord  7644  caovord3  7646  f1oweALT  7996  oaordex  8595  oaass  8598  odi  8616  findcard2s  9204  unfilem1  9341  suppeqfsuppbi  9417  oieu  9577  r1pw  9883  carddomi2  10008  isacn  10082  djudom2  10222  axdc2  10487  alephval2  10610  distrlem4pr  11064  axpre-sup  11207  nn0ind-raph  12716  elpq  13015  xnn0xadd0  13286  elfz  13550  elfzp12  13640  expeq0  14130  leiso  14495  wrd2ind  14758  trcleq12lem  15029  dfrtrclrec2  15094  shftfib  15108  absdvdsb  16309  dvdsabsb  16310  dvdsabseq  16347  unbenlem  16942  isprs  18354  isdrs  18359  pltval  18390  lublecllem  18418  istos  18476  isdlat  18580  znfld  21597  tgss2  23010  isopn2  23056  cnpf2  23274  lmbr  23282  isreg2  23401  fclsrest  24048  qustgplem  24145  ustuqtoplem  24264  xmetec  24460  nmogelb  24753  metdstri  24887  tcphcph  25285  ulmval  26438  2lgslem1a  27450  elmade  27921  iscgrg  28535  istrlson  29740  ispthson  29775  isspthson  29776  elwwlks2on  29989  eupth2lem1  30247  eigrei  31863  eigorthi  31866  jplem1  32297  superpos  32383  chrelati  32393  bian1d  32484  br8d  32630  ellpi  33381  issiga  34093  eulerpartlemgvv  34358  cplgredgex  35105  acycgrcycl  35132  br8  35736  br6  35737  br4  35738  brsegle  36090  topfne  36337  tailfb  36360  filnetlem1  36361  nndivsub  36440  bj-rest10  37071  isbasisrelowllem1  37338  isbasisrelowllem2  37339  fvineqsnf1  37393  wl-2sb6d  37539  curf  37585  curunc  37589  poimirlem26  37633  mblfinlem2  37645  cnambfre  37655  itgaddnclem2  37666  ftc1anclem1  37680  grpokerinj  37880  rngoisoval  37964  smprngopr  38039  parteq12  38758  ax12eq  38923  ax12el  38924  2llnjN  39550  2lplnj  39603  elpadd0  39792  lauteq  40078  lpolconN  41470  f1o2d2  42253  rexrabdioph  42782  tfsnfin  43342  eliunov2  43669  nzss  44313  iotasbc2  44416  or2expropbilem2  46983  elsetpreimafvbi  47316  reuopreuprim  47451  grlicref  47908  cbvmpox2  48181  naryfvalel  48480  line2x  48604