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  1436  nanbi12  1504  elequ12  2131  sbcom2  2178  2sb5rf  2476  2sb6rf  2477  eqeqan12d  2750  eleq12  2826  ceqsrex2v  3612  elabd2  3624  elabgt  3626  sseq12  3961  csbie2df  4395  2ralsng  4635  rexprgf  4652  rextpg  4656  breq12  5103  reusv2lem5  5347  opelopabg  5486  brabg  5487  opelopabgf  5488  opelopab2  5489  rbropapd  5510  poeq12d  5537  soeq12d  5555  freq12d  5593  seeq12d  5596  weeq12d  5613  ralxpf  5795  feq23  6643  f00  6716  fconstg  6721  f1oeq23  6765  f1o00  6809  fnelfp  7121  fnelnfp  7123  isofrlem  7286  f1oiso  7297  riota1a  7337  cbvmpox  7451  caovord  7569  caovord3  7571  f1oweALT  7916  oaordex  8485  oaass  8488  odi  8506  findcard2s  9090  unfilem1  9205  tfsnfin2  9263  suppeqfsuppbi  9282  oieu  9444  r1pw  9757  carddomi2  9882  isacn  9954  djudom2  10094  axdc2  10359  alephval2  10483  distrlem4pr  10937  axpre-sup  11080  nn0ind-raph  12592  elpq  12888  xnn0xadd0  13162  elfz  13429  elfzp12  13519  expeq0  14015  leiso  14382  wrd2ind  14646  trcleq12lem  14916  dfrtrclrec2  14981  shftfib  14995  absdvdsb  16201  dvdsabsb  16202  dvdsabseq  16240  unbenlem  16836  isprs  18219  isdrs  18224  pltval  18253  lublecllem  18281  istos  18339  isdlat  18445  znfld  21515  tgss2  22931  isopn2  22976  cnpf2  23194  lmbr  23202  isreg2  23321  fclsrest  23968  qustgplem  24065  ustuqtoplem  24183  xmetec  24378  nmogelb  24660  metdstri  24796  tcphcph  25193  ulmval  26345  2lgslem1a  27358  elmade  27853  bdayle  27912  iscgrg  28584  istrlson  29778  ispthson  29815  isspthson  29816  elwwlks2on  30034  eupth2lem1  30293  eigrei  31909  eigorthi  31912  jplem1  32343  superpos  32429  chrelati  32439  bian1d  32530  br8d  32686  ellpi  33454  issiga  34269  eulerpartlemgvv  34533  cplgredgex  35315  acycgrcycl  35341  br8  35950  br6  35951  br4  35952  brsegle  36302  topfne  36548  tailfb  36571  filnetlem1  36572  nndivsub  36651  bj-rest10  37293  isbasisrelowllem1  37560  isbasisrelowllem2  37561  fvineqsnf1  37615  wl-2sb6d  37763  curf  37799  curunc  37803  poimirlem26  37847  mblfinlem2  37859  cnambfre  37869  itgaddnclem2  37880  ftc1anclem1  37894  grpokerinj  38094  rngoisoval  38178  smprngopr  38253  parteq12  39035  ax12eq  39201  ax12el  39202  2llnjN  39827  2lplnj  39880  elpadd0  40069  lauteq  40355  lpolconN  41747  f1o2d2  42489  rexrabdioph  43036  tfsnfin  43594  eliunov2  43920  nzss  44558  iotasbc2  44661  or2expropbilem2  47279  elsetpreimafvbi  47637  reuopreuprim  47772  grlicref  48258  cbvmpox2  48582  naryfvalel  48876  line2x  49000  brab2ddw  49074  brab2ddw2  49075