Theorem sylan9bb 505

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  sylan9bbr  506  baibd  535  rbaibd  536  bi2anan9  629  syl3an9b  1507  nanbi12  1573  sbcom2  2523  sbcom2OLD  2524  2sb5rf  2530  2sb6rf  2531  2sb6rfOLD  2532  eqeq12  2791  eleq12  2849  sbhypf  3455  ceqsrex2v  3541  sseq12  3847  2ralsng  4447  rexprgf  4462  rextpg  4466  breq12  4893  reusv2lem5  5116  opelopabg  5232  brabg  5233  opelopabgf  5234  opelopab2  5235  rbropapd  5254  ralxpf  5516  feq23  6277  f00  6339  fconstg  6344  f1oeq23  6385  f1o00  6427  fnelfp  6710  fnelnfp  6712  isofrlem  6864  f1oiso  6875  riota1a  6904  cbvmpt2x  7012  caovord  7124  caovord3  7126  f1oweALT  7431  oaordex  7924  oaass  7927  odi  7945  findcard2s  8491  unfilem1  8514  suppeqfsuppbi  8579  oieu  8735  r1pw  9007  carddomi2  9131  isacn  9202  cdadom2  9346  axdc2  9608  alephval2  9731  fpwwe2cbv  9789  fpwwe2lem2  9791  fpwwecbv  9803  fpwwelem  9804  canthwelem  9809  canthwe  9810  distrlem4pr  10185  axpre-sup  10328  nn0ind-raph  11833  elpq  12126  xnn0xadd0  12393  elfz  12653  elfzp12  12741  expeq0  13212  leiso  13561  wrd2ind  13848  wrd2indOLD  13849  trcleq12lem  14145  dfrtrclrec2  14208  shftfib  14223  absdvdsb  15411  dvdsabsb  15412  dvdsabseq  15446  unbenlem  16020  isprs  17320  isdrs  17324  pltval  17350  lublecllem  17378  istos  17425  isdlat  17583  znfld  20308  tgss2  21203  isopn2  21248  cnpf2  21466  lmbr  21474  isreg2  21593  fclsrest  22240  qustgplem  22336  ustuqtoplem  22455  xmetec  22651  nmogelb  22932  metdstri  23066  tcphcph  23447  ulmval  24575  2lgslem1a  25572  iscgrg  25867  istrlson  27063  ispthson  27098  isspthson  27099  elwwlks2on  27343  eupth2lem1  27626  eigrei  29269  eigorthi  29272  jplem1  29703  superpos  29789  chrelati  29799  vtocl2d  29890  br8d  29989  issiga  30776  eulerpartlemgvv  31040  br8  32244  br6  32245  br4  32246  brsegle  32808  topfne  32941  tailfb  32964  filnetlem1  32965  nndivsub  33043  bj-elequ12  33261  bj-rest10  33618  isbasisrelowllem1  33801  isbasisrelowllem2  33802  wl-2sb6d  33938  curf  34017  curunc  34021  poimirlem26  34066  mblfinlem2  34078  cnambfre  34088  itgaddnclem2  34099  ftc1anclem1  34115  grpokerinj  34321  rngoisoval  34405  smprngopr  34480  ax12eq  35100  ax12el  35101  2llnjN  35726  2lplnj  35779  elpadd0  35968  lauteq  36254  lpolconN  37646  rexrabdioph  38328  eliunov2  38938  nzss  39482  iotasbc2  39586  cbvmpt2x2  43139  line2x  43500