Theorem sylan9bb 514

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  sylan9bbr  515  baibd  544  syl3an9b  1442  nanbi12  1510  elequ12  2137  sbcom2  2183  2sb5rf  2480  2sb6rf  2481  eqeqan12d  2753  eleq12  2829  ceqsrex2v  3596  elabd2  3608  elabgt  3610  sseq12  3942  csbie2df  4371  2ralsng  4610  rexprgf  4627  rextpg  4631  breq12  5077  reusv2lem5  5331  opelopabg  5480  brabg  5481  opelopabgf  5482  opelopab2  5483  rbropapd  5504  poeq12d  5531  soeq12d  5549  freq12d  5587  seeq12d  5590  weeq12d  5607  ralxpf  5788  feq23  6636  f00  6709  fconstg  6714  f1oeq23  6758  f1o00  6802  fnelfp  7119  fnelnfp  7121  isofrlem  7284  f1oiso  7295  riota1a  7335  cbvmpox  7449  caovord  7567  caovord3  7569  f1oweALT  7914  mpof1o2d  8065  oaordex  8483  oaass  8486  odi  8504  findcard2s  9090  unfilem1  9205  tfsnfin2  9263  suppeqfsuppbi  9282  oieu  9444  r1pw  9760  carddomi2  9885  isacn  9957  djudom2  10097  axdc2  10362  alephval2  10486  distrlem4pr  10940  axpre-sup  11083  nn0ind-raph  12620  elpq  12916  xnn0xadd0  13190  elfz  13458  elfzp12  13548  expeq0  14045  leiso  14412  wrd2ind  14676  trcleq12lem  14946  dfrtrclrec2  15011  shftfib  15025  absdvdsb  16234  dvdsabsb  16235  dvdsabseq  16273  unbenlem  16870  isprs  18253  isdrs  18258  pltval  18287  lublecllem  18315  istos  18373  isdlat  18479  znfld  21535  tgss2  22970  isopn2  23015  cnpf2  23233  lmbr  23241  isreg2  23360  fclsrest  24007  qustgplem  24104  ustuqtoplem  24222  xmetec  24417  nmogelb  24699  metdstri  24835  tcphcph  25222  ulmval  26363  2lgslem1a  27372  elmade  27867  bdayle  27926  iscgrg  28598  istrlson  29791  ispthson  29828  isspthson  29829  elwwlks2on  30047  eupth2lem1  30306  eigrei  31923  eigorthi  31926  jplem1  32357  superpos  32443  chrelati  32453  br8d  32700  ellpi  33456  issiga  34296  eulerpartlemgvv  34560  cplgredgex  35349  acycgrcycl  35375  br8  35984  br6  35985  br4  35986  brsegle  36336  topfne  36582  tailfb  36605  filnetlem1  36606  nndivsub  36685  bj-rest10  37446  isbasisrelowllem1  37717  isbasisrelowllem2  37718  fvineqsnf1  37772  wl-2sb6d  37929  curf  37965  curunc  37969  poimirlem26  38013  mblfinlem2  38025  cnambfre  38035  itgaddnclem2  38046  ftc1anclem1  38060  grpokerinj  38260  rngoisoval  38344  smprngopr  38419  parteq12  39246  ax12eq  39433  ax12el  39434  2llnjN  40059  2lplnj  40112  elpadd0  40301  lauteq  40587  lpolconN  41979  rexrabdioph  43239  tfsnfin  43797  eliunov2  44123  nzss  44761  iotasbc2  44864  or2expropbilem2  47496  elsetpreimafvbi  47866  reuopreuprim  48001  grlicref  48503  cbvmpox2  48827  naryfvalel  49121  line2x  49245  brab2ddw  49319  brab2ddw2  49320