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  1503  elequ12  2127  sbcom2  2174  2sb5rf  2470  2sb6rf  2471  eqeqan12d  2743  eleq12  2818  sbhypfOLD  3511  ceqsrex2v  3624  elabd2  3636  elabgt  3638  sseq12  3974  csbie2df  4406  2ralsng  4642  rexprgf  4659  rextpg  4663  breq12  5112  reusv2lem5  5357  opelopabg  5498  brabg  5499  opelopabgf  5500  opelopab2  5501  rbropapd  5524  poeq12d  5551  soeq12d  5569  freq12d  5607  seeq12d  5610  weeq12d  5627  ralxpf  5810  feq23  6669  f00  6742  fconstg  6747  f1oeq23  6791  f1o00  6835  fnelfp  7149  fnelnfp  7151  isofrlem  7315  f1oiso  7326  riota1a  7366  cbvmpox  7482  caovord  7600  caovord3  7602  f1oweALT  7951  oaordex  8522  oaass  8525  odi  8543  findcard2s  9129  unfilem1  9254  suppeqfsuppbi  9330  oieu  9492  r1pw  9798  carddomi2  9923  isacn  9997  djudom2  10137  axdc2  10402  alephval2  10525  distrlem4pr  10979  axpre-sup  11122  nn0ind-raph  12634  elpq  12934  xnn0xadd0  13207  elfz  13474  elfzp12  13564  expeq0  14057  leiso  14424  wrd2ind  14688  trcleq12lem  14959  dfrtrclrec2  15024  shftfib  15038  absdvdsb  16244  dvdsabsb  16245  dvdsabseq  16283  unbenlem  16879  isprs  18257  isdrs  18262  pltval  18291  lublecllem  18319  istos  18377  isdlat  18481  znfld  21470  tgss2  22874  isopn2  22919  cnpf2  23137  lmbr  23145  isreg2  23264  fclsrest  23911  qustgplem  24008  ustuqtoplem  24127  xmetec  24322  nmogelb  24604  metdstri  24740  tcphcph  25137  ulmval  26289  2lgslem1a  27302  elmade  27779  iscgrg  28439  istrlson  29635  ispthson  29672  isspthson  29673  elwwlks2on  29889  eupth2lem1  30147  eigrei  31763  eigorthi  31766  jplem1  32197  superpos  32283  chrelati  32293  bian1d  32385  br8d  32538  ellpi  33344  issiga  34102  eulerpartlemgvv  34367  cplgredgex  35108  acycgrcycl  35134  br8  35743  br6  35744  br4  35745  brsegle  36096  topfne  36342  tailfb  36365  filnetlem1  36366  nndivsub  36445  bj-rest10  37076  isbasisrelowllem1  37343  isbasisrelowllem2  37344  fvineqsnf1  37398  wl-2sb6d  37546  curf  37592  curunc  37596  poimirlem26  37640  mblfinlem2  37652  cnambfre  37662  itgaddnclem2  37673  ftc1anclem1  37687  grpokerinj  37887  rngoisoval  37971  smprngopr  38046  parteq12  38768  ax12eq  38934  ax12el  38935  2llnjN  39561  2lplnj  39614  elpadd0  39803  lauteq  40089  lpolconN  41481  f1o2d2  42221  rexrabdioph  42782  tfsnfin  43341  eliunov2  43668  nzss  44306  iotasbc2  44409  or2expropbilem2  47034  elsetpreimafvbi  47392  reuopreuprim  47527  grlicref  48004  cbvmpox2  48324  naryfvalel  48619  line2x  48743  brab2ddw  48817  brab2ddw2  48818