Theorem sylan9bb 513

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  sylan9bbr  514  baibd  543  syl3an9b  1431  nanbi12  1494  sbcom2  2165  2sb5rf  2485  2sb6rf  2486  eqeq12  2812  eleq12  2879  sbhypf  3500  ceqsrex2v  3599  vtocl2dOLD  3876  sseq12  3942  csbie2df  4348  2ralsng  4576  rexprgf  4591  rextpg  4595  breq12  5035  reusv2lem5  5268  opelopabg  5390  brabg  5391  opelopabgf  5392  opelopab2  5393  rbropapd  5414  ralxpf  5681  feq23  6471  f00  6535  fconstg  6540  f1oeq23  6582  f1o00  6624  fnelfp  6914  fnelnfp  6916  isofrlem  7072  f1oiso  7083  riota1a  7115  cbvmpox  7226  caovord  7339  caovord3  7341  f1oweALT  7655  oaordex  8167  oaass  8170  odi  8188  findcard2s  8743  unfilem1  8766  suppeqfsuppbi  8831  oieu  8987  r1pw  9258  carddomi2  9383  isacn  9455  djudom2  9594  axdc2  9860  alephval2  9983  fpwwe2cbv  10041  fpwwe2lem2  10043  fpwwecbv  10055  fpwwelem  10056  canthwelem  10061  canthwe  10062  distrlem4pr  10437  axpre-sup  10580  nn0ind-raph  12070  elpq  12362  xnn0xadd0  12628  elfz  12891  elfzp12  12981  expeq0  13455  leiso  13813  wrd2ind  14076  trcleq12lem  14344  dfrtrclrec2  14409  shftfib  14423  absdvdsb  15620  dvdsabsb  15621  dvdsabseq  15655  unbenlem  16234  isprs  17532  isdrs  17536  pltval  17562  lublecllem  17590  istos  17637  isdlat  17795  znfld  20252  tgss2  21592  isopn2  21637  cnpf2  21855  lmbr  21863  isreg2  21982  fclsrest  22629  qustgplem  22726  ustuqtoplem  22845  xmetec  23041  nmogelb  23322  metdstri  23456  tcphcph  23841  ulmval  24975  2lgslem1a  25975  iscgrg  26306  istrlson  27496  ispthson  27531  isspthson  27532  elwwlks2on  27745  eupth2lem1  28003  eigrei  29617  eigorthi  29620  jplem1  30051  superpos  30137  chrelati  30147  br8d  30374  issiga  31481  eulerpartlemgvv  31744  cplgredgex  32480  acycgrcycl  32507  br8  33105  br6  33106  br4  33107  brsegle  33682  topfne  33815  tailfb  33838  filnetlem1  33839  nndivsub  33918  bj-elequ12  34125  bj-rest10  34503  isbasisrelowllem1  34772  isbasisrelowllem2  34773  fvineqsnf1  34827  wl-2sb6d  34959  curf  35035  curunc  35039  poimirlem26  35083  mblfinlem2  35095  cnambfre  35105  itgaddnclem2  35116  ftc1anclem1  35130  grpokerinj  35331  rngoisoval  35415  smprngopr  35490  ax12eq  36237  ax12el  36238  2llnjN  36863  2lplnj  36916  elpadd0  37105  lauteq  37391  lpolconN  38783  rexrabdioph  39735  eliunov2  40380  nzss  41021  iotasbc2  41124  or2expropbilem2  43625  elsetpreimafvbi  43908  reuopreuprim  44043  cbvmpox2  44737  naryfvalel  45044  line2x  45168