Theorem sylan9bb 736

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 268	1 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  sylan9bbr  737  bi2anan9  935  baibd  968  rbaibd  969  syl3an9b  1437  nanbi12  1497  sbcom2  2473  2sb5rf  2479  2sb6rf  2480  eqeq12  2664  eleq12  2720  sbhypf  3284  ceqsrex2v  3369  sseq12  3661  2ralsng  4252  rexprg  4267  rextpg  4269  breq12  4690  reusv2lem5  4903  opelopabg  5022  brabg  5023  opelopabgf  5024  opelopab2  5025  rbropapd  5044  ralxpf  5301  feq23  6067  f00  6125  fconstg  6130  f1oeq23  6168  f1o00  6209  fnelfp  6482  fnelnfp  6484  isofrlem  6630  f1oiso  6641  riota1a  6670  cbvmpt2x  6775  caovord  6887  caovord3  6889  f1oweALT  7194  oaordex  7683  oaass  7686  odi  7704  findcard2s  8242  unfilem1  8265  suppeqfsuppbi  8330  oieu  8485  r1pw  8746  carddomi2  8834  isacn  8905  cdadom2  9047  axdc2  9309  alephval2  9432  fpwwe2cbv  9490  fpwwe2lem2  9492  fpwwecbv  9504  fpwwelem  9505  canthwelem  9510  canthwe  9511  distrlem4pr  9886  axpre-sup  10028  nn0ind-raph  11515  xnn0xadd0  12115  elfz  12370  elfzp12  12457  expeq0  12930  leiso  13281  wrd2ind  13523  trcleq12lem  13778  dfrtrclrec2  13841  shftfib  13856  absdvdsb  15047  dvdsabsb  15048  dvdsabseq  15082  unbenlem  15659  isprs  16977  isdrs  16981  pltval  17007  lublecllem  17035  istos  17082  isdlat  17240  znfld  19957  tgss2  20839  isopn2  20884  cnpf2  21102  lmbr  21110  isreg2  21229  fclsrest  21875  qustgplem  21971  ustuqtoplem  22090  xmetec  22286  nmogelb  22567  metdstri  22701  tchcph  23082  ulmval  24179  2lgslem1a  25161  iscgrg  25452  istrlson  26659  ispthson  26694  isspthson  26695  elwwlks2on  26925  eupth2lem1  27196  eigrei  28821  eigorthi  28824  jplem1  29255  superpos  29341  chrelati  29351  vtocl2d  29442  br8d  29548  issiga  30302  eulerpartlemgvv  30566  br8  31772  br6  31773  br4  31774  brsegle  32340  topfne  32474  tailfb  32497  filnetlem1  32498  nndivsub  32581  bj-elequ12  32793  bj-rest10  33166  isbasisrelowllem1  33333  isbasisrelowllem2  33334  wl-2sb6d  33471  curf  33517  curunc  33521  poimirlem26  33565  mblfinlem2  33577  cnambfre  33588  itgaddnclem2  33599  ftc1anclem1  33615  grpokerinj  33822  rngoisoval  33906  smprngopr  33981  ax12eq  34545  ax12el  34546  2llnjN  35171  2lplnj  35224  elpadd0  35413  lauteq  35699  lpolconN  37093  rexrabdioph  37675  eliunov2  38288  nzss  38833  iotasbc2  38938  cbvmpt2x2  42439