Theorem sylan9bb 501

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

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384

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

This theorem is referenced by:  sylan9bbr  502  baibd  531  rbaibd  532  bi2anan9  622  syl3an9b  1551  nanbi12  1611  sbcom2  2605  2sb5rf  2611  2sb6rf  2612  eqeq12  2817  eleq12  2873  sbhypf  3445  ceqsrex2v  3530  sseq12  3823  2ralsng  4411  rexprg  4425  rextpg  4427  breq12  4847  reusv2lem5  5069  opelopabg  5186  brabg  5187  opelopabgf  5188  opelopab2  5189  rbropapd  5208  ralxpf  5468  feq23  6238  f00  6300  fconstg  6305  f1oeq23  6344  f1o00  6385  fnelfp  6664  fnelnfp  6666  isofrlem  6812  f1oiso  6823  riota1a  6852  cbvmpt2x  6961  caovord  7073  caovord3  7075  f1oweALT  7380  oaordex  7873  oaass  7876  odi  7894  findcard2s  8438  unfilem1  8461  suppeqfsuppbi  8526  oieu  8681  r1pw  8953  carddomi2  9077  isacn  9148  cdadom2  9292  axdc2  9554  alephval2  9677  fpwwe2cbv  9735  fpwwe2lem2  9737  fpwwecbv  9749  fpwwelem  9750  canthwelem  9755  canthwe  9756  distrlem4pr  10131  axpre-sup  10273  nn0ind-raph  11741  xnn0xadd0  12293  elfz  12553  elfzp12  12640  expeq0  13111  leiso  13458  wrd2ind  13699  trcleq12lem  13955  dfrtrclrec2  14018  shftfib  14033  absdvdsb  15221  dvdsabsb  15222  dvdsabseq  15256  unbenlem  15827  isprs  17133  isdrs  17137  pltval  17163  lublecllem  17191  istos  17238  isdlat  17396  znfld  20114  tgss2  21003  isopn2  21048  cnpf2  21266  lmbr  21274  isreg2  21393  fclsrest  22039  qustgplem  22135  ustuqtoplem  22254  xmetec  22450  nmogelb  22731  metdstri  22865  tchcph  23246  ulmval  24346  2lgslem1a  25328  iscgrg  25619  istrlson  26829  ispthson  26864  isspthson  26865  elwwlks2on  27098  eupth2lem1  27389  eigrei  29019  eigorthi  29022  jplem1  29453  superpos  29539  chrelati  29549  vtocl2d  29640  br8d  29745  issiga  30497  eulerpartlemgvv  30761  br8  31966  br6  31967  br4  31968  brsegle  32534  topfne  32668  tailfb  32691  filnetlem1  32692  nndivsub  32771  bj-elequ12  32981  bj-rest10  33350  isbasisrelowllem1  33517  isbasisrelowllem2  33518  wl-2sb6d  33653  curf  33698  curunc  33702  poimirlem26  33746  mblfinlem2  33758  cnambfre  33768  itgaddnclem2  33779  ftc1anclem1  33795  grpokerinj  34001  rngoisoval  34085  smprngopr  34160  ax12eq  34718  ax12el  34719  2llnjN  35345  2lplnj  35398  elpadd0  35587  lauteq  35873  lpolconN  37266  rexrabdioph  37858  eliunov2  38469  nzss  39014  iotasbc2  39118  cbvmpt2x2  42680