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  1504  elequ12  2129  sbcom2  2176  2sb5rf  2472  2sb6rf  2473  eqeqan12d  2745  eleq12  2821  ceqsrex2v  3608  elabd2  3620  elabgt  3622  sseq12  3957  csbie2df  4388  2ralsng  4626  rexprgf  4643  rextpg  4647  breq12  5091  reusv2lem5  5335  opelopabg  5473  brabg  5474  opelopabgf  5475  opelopab2  5476  rbropapd  5497  poeq12d  5524  soeq12d  5542  freq12d  5580  seeq12d  5583  weeq12d  5600  ralxpf  5781  feq23  6627  f00  6700  fconstg  6705  f1oeq23  6749  f1o00  6793  fnelfp  7104  fnelnfp  7106  isofrlem  7269  f1oiso  7280  riota1a  7320  cbvmpox  7434  caovord  7552  caovord3  7554  f1oweALT  7899  oaordex  8468  oaass  8471  odi  8489  findcard2s  9070  unfilem1  9184  suppeqfsuppbi  9258  oieu  9420  r1pw  9733  carddomi2  9858  isacn  9930  djudom2  10070  axdc2  10335  alephval2  10458  distrlem4pr  10912  axpre-sup  11055  nn0ind-raph  12568  elpq  12868  xnn0xadd0  13141  elfz  13408  elfzp12  13498  expeq0  13994  leiso  14361  wrd2ind  14625  trcleq12lem  14895  dfrtrclrec2  14960  shftfib  14974  absdvdsb  16180  dvdsabsb  16181  dvdsabseq  16219  unbenlem  16815  isprs  18197  isdrs  18202  pltval  18231  lublecllem  18259  istos  18317  isdlat  18423  znfld  21492  tgss2  22897  isopn2  22942  cnpf2  23160  lmbr  23168  isreg2  23287  fclsrest  23934  qustgplem  24031  ustuqtoplem  24149  xmetec  24344  nmogelb  24626  metdstri  24762  tcphcph  25159  ulmval  26311  2lgslem1a  27324  elmade  27807  bdayle  27856  iscgrg  28485  istrlson  29678  ispthson  29715  isspthson  29716  elwwlks2on  29932  eupth2lem1  30190  eigrei  31806  eigorthi  31809  jplem1  32240  superpos  32326  chrelati  32336  bian1d  32427  br8d  32583  ellpi  33330  issiga  34117  eulerpartlemgvv  34381  cplgredgex  35157  acycgrcycl  35183  br8  35792  br6  35793  br4  35794  brsegle  36142  topfne  36388  tailfb  36411  filnetlem1  36412  nndivsub  36491  bj-rest10  37122  isbasisrelowllem1  37389  isbasisrelowllem2  37390  fvineqsnf1  37444  wl-2sb6d  37592  curf  37638  curunc  37642  poimirlem26  37686  mblfinlem2  37698  cnambfre  37708  itgaddnclem2  37719  ftc1anclem1  37733  grpokerinj  37933  rngoisoval  38017  smprngopr  38092  parteq12  38814  ax12eq  38980  ax12el  38981  2llnjN  39606  2lplnj  39659  elpadd0  39848  lauteq  40134  lpolconN  41526  f1o2d2  42266  rexrabdioph  42827  tfsnfin  43385  eliunov2  43712  nzss  44350  iotasbc2  44453  or2expropbilem2  47064  elsetpreimafvbi  47422  reuopreuprim  47557  grlicref  48043  cbvmpox2  48367  naryfvalel  48662  line2x  48786  brab2ddw  48860  brab2ddw2  48861