Theorem sylan9bb 510

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

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

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 397

This theorem is referenced by:  sylan9bbr  511  baibd  540  syl3an9b  1433  nanbi12  1498  sbcom2  2162  2sb5rf  2473  2sb6rf  2474  eqeqan12d  2753  eqeq12OLD  2758  eleq12  2829  sbhypf  3492  ceqsrex2v  3588  elabd2  3602  sseq12  3949  csbie2df  4375  2ralsng  4613  rexprgf  4630  rextpg  4636  breq12  5080  reusv2lem5  5326  opelopabg  5452  brabg  5453  opelopabgf  5454  opelopab2  5455  rbropapd  5478  ralxpf  5758  feq23  6593  f00  6665  fconstg  6670  f1oeq23  6716  f1o00  6760  fnelfp  7056  fnelnfp  7058  isofrlem  7220  f1oiso  7231  riota1a  7264  cbvmpox  7377  caovord  7492  caovord3  7494  f1oweALT  7824  oaordex  8398  oaass  8401  odi  8419  findcard2s  8957  unfilem1  9087  suppeqfsuppbi  9151  oieu  9307  r1pw  9612  carddomi2  9737  isacn  9809  djudom2  9948  axdc2  10214  alephval2  10337  fpwwe2cbv  10395  fpwwe2lem2  10397  fpwwecbv  10409  fpwwelem  10410  canthwelem  10415  canthwe  10416  distrlem4pr  10791  axpre-sup  10934  nn0ind-raph  12429  elpq  12724  xnn0xadd0  12990  elfz  13254  elfzp12  13344  expeq0  13822  leiso  14182  wrd2ind  14445  trcleq12lem  14713  dfrtrclrec2  14778  shftfib  14792  absdvdsb  15993  dvdsabsb  15994  dvdsabseq  16031  unbenlem  16618  isprs  18024  isdrs  18028  pltval  18059  lublecllem  18087  istos  18145  isdlat  18249  znfld  20777  tgss2  22146  isopn2  22192  cnpf2  22410  lmbr  22418  isreg2  22537  fclsrest  23184  qustgplem  23281  ustuqtoplem  23400  xmetec  23596  nmogelb  23889  metdstri  24023  tcphcph  24410  ulmval  25548  2lgslem1a  26548  iscgrg  26882  istrlson  28084  ispthson  28119  isspthson  28120  elwwlks2on  28333  eupth2lem1  28591  eigrei  30205  eigorthi  30208  jplem1  30639  superpos  30725  chrelati  30735  br8d  30959  issiga  32089  eulerpartlemgvv  32352  cplgredgex  33091  acycgrcycl  33118  br8  33732  br6  33733  br4  33734  elmade  34060  brsegle  34419  topfne  34552  tailfb  34575  filnetlem1  34576  nndivsub  34655  bj-elequ12  34869  bj-rest10  35268  isbasisrelowllem1  35535  isbasisrelowllem2  35536  fvineqsnf1  35590  wl-2sb6d  35722  curf  35764  curunc  35768  poimirlem26  35812  mblfinlem2  35824  cnambfre  35834  itgaddnclem2  35845  ftc1anclem1  35859  grpokerinj  36060  rngoisoval  36144  smprngopr  36219  ax12eq  36962  ax12el  36963  2llnjN  37588  2lplnj  37641  elpadd0  37830  lauteq  38116  lpolconN  39508  rexrabdioph  40623  eliunov2  41294  nzss  41942  iotasbc2  42045  or2expropbilem2  44538  elsetpreimafvbi  44854  reuopreuprim  44989  cbvmpox2  45682  naryfvalel  45987  line2x  46111