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  1437  nanbi12  1505  elequ12  2132  sbcom2  2179  2sb5rf  2477  2sb6rf  2478  eqeqan12d  2751  eleq12  2827  ceqsrex2v  3614  elabd2  3626  elabgt  3628  sseq12  3963  csbie2df  4397  2ralsng  4637  rexprgf  4654  rextpg  4658  breq12  5105  reusv2lem5  5349  opelopabg  5494  brabg  5495  opelopabgf  5496  opelopab2  5497  rbropapd  5518  poeq12d  5545  soeq12d  5563  freq12d  5601  seeq12d  5604  weeq12d  5621  ralxpf  5803  feq23  6651  f00  6724  fconstg  6729  f1oeq23  6773  f1o00  6817  fnelfp  7131  fnelnfp  7133  isofrlem  7296  f1oiso  7307  riota1a  7347  cbvmpox  7461  caovord  7579  caovord3  7581  f1oweALT  7926  oaordex  8495  oaass  8498  odi  8516  findcard2s  9102  unfilem1  9217  tfsnfin2  9275  suppeqfsuppbi  9294  oieu  9456  r1pw  9769  carddomi2  9894  isacn  9966  djudom2  10106  axdc2  10371  alephval2  10495  distrlem4pr  10949  axpre-sup  11092  nn0ind-raph  12604  elpq  12900  xnn0xadd0  13174  elfz  13441  elfzp12  13531  expeq0  14027  leiso  14394  wrd2ind  14658  trcleq12lem  14928  dfrtrclrec2  14993  shftfib  15007  absdvdsb  16213  dvdsabsb  16214  dvdsabseq  16252  unbenlem  16848  isprs  18231  isdrs  18236  pltval  18265  lublecllem  18293  istos  18351  isdlat  18457  znfld  21527  tgss2  22943  isopn2  22988  cnpf2  23206  lmbr  23214  isreg2  23333  fclsrest  23980  qustgplem  24077  ustuqtoplem  24195  xmetec  24390  nmogelb  24672  metdstri  24808  tcphcph  25205  ulmval  26357  2lgslem1a  27370  elmade  27865  bdayle  27924  iscgrg  28596  istrlson  29790  ispthson  29827  isspthson  29828  elwwlks2on  30046  eupth2lem1  30305  eigrei  31922  eigorthi  31925  jplem1  32356  superpos  32442  chrelati  32452  br8d  32698  ellpi  33466  issiga  34290  eulerpartlemgvv  34554  cplgredgex  35337  acycgrcycl  35363  br8  35972  br6  35973  br4  35974  brsegle  36324  topfne  36570  tailfb  36593  filnetlem1  36594  nndivsub  36673  bj-rest10  37341  isbasisrelowllem1  37610  isbasisrelowllem2  37611  fvineqsnf1  37665  wl-2sb6d  37813  curf  37849  curunc  37853  poimirlem26  37897  mblfinlem2  37909  cnambfre  37919  itgaddnclem2  37930  ftc1anclem1  37944  grpokerinj  38144  rngoisoval  38228  smprngopr  38303  parteq12  39130  ax12eq  39317  ax12el  39318  2llnjN  39943  2lplnj  39996  elpadd0  40185  lauteq  40471  lpolconN  41863  f1o2d2  42605  rexrabdioph  43151  tfsnfin  43709  eliunov2  44035  nzss  44673  iotasbc2  44776  or2expropbilem2  47393  elsetpreimafvbi  47751  reuopreuprim  47886  grlicref  48372  cbvmpox2  48696  naryfvalel  48990  line2x  49114  brab2ddw  49188  brab2ddw2  49189