Theorem sylan9bb 518

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  sylan9bbr  519  baibd  548  syl3an9b  1462  nanbi12  1533  elequ12  2161  sbcom2  2207  2sb5rf  2504  2sb6rf  2505  eqeqan12d  2777  eleq12  2853  ceqsrex2v  3618  elabd2  3630  elabgt  3632  sseq12  3965  csbie2df  4409  2ralsng  4645  rexprgf  4662  rextpg  4666  breq12  5115  reusv2lem5  5375  opelopabg  5525  brabg  5526  opelopabgf  5527  opelopab2  5528  rbropapd  5549  poeq12d  5576  soeq12d  5594  freq12d  5632  seeq12d  5635  weeq12d  5652  ralxpf  5834  feq23  6688  f00  6762  fconstg  6767  f1oeq23  6813  f1o00  6858  fnelfp  7175  fnelnfp  7177  isofrlem  7340  f1oiso  7351  riota1a  7391  cbvmpox  7505  caovord  7623  caovord3  7625  f1oweALT  7970  mpof1o2d  8122  oaordex  8544  oaass  8547  odi  8565  findcard2s  9151  unfilem1  9266  tfsnfin2  9321  suppeqfsuppbi  9340  oieu  9502  r1pw  9818  carddomi2  9957  isacn  10029  djudom2  10168  axdc2  10434  alephval2  10558  distrlem4pr  11012  axpre-sup  11155  nn0ind-raph  12697  elpq  13000  xnn0xadd0  13274  elfz  13542  elfzp12  13633  expeq0  14130  leiso  14498  wrd2ind  14762  trcleq12lem  15032  dfrtrclrec2  15097  shftfib  15111  absdvdsb  16333  dvdsabsb  16334  dvdsabseq  16372  unbenlem  16969  isprs  18353  isdrs  18358  pltval  18387  lublecllem  18415  istos  18473  isdlat  18579  znfld  21691  tgss2  23125  isopn2  23170  cnpf2  23388  lmbr  23396  isreg2  23515  fclsrest  24162  qustgplem  24259  ustuqtoplem  24377  xmetec  24572  nmogelb  24854  metdstri  24990  tcphcph  25377  ulmval  26524  2lgslem1a  27536  elmade  28031  bdayle  28090  iscgrg  28762  istrlson  30035  ispthson  30072  isspthson  30073  elwwlks2on  30291  eupth2lem1  30550  eigrei  32167  eigorthi  32170  jplem1  32601  superpos  32687  chrelati  32697  br8d  32934  ellpi  33668  issiga  34483  eulerpartlemgvv  34747  cplgredgex  35594  acycgrcycl  35620  br8  36229  br6  36230  br4  36231  brsegle  36581  topfne  36846  tailfb  36869  filnetlem1  36870  nndivsub  36949  bj-rest10  37711  isbasisrelowllem1  37982  isbasisrelowllem2  37983  fvineqsnf1  38037  wl-2sb6d  38194  curf  38230  curunc  38234  poimirlem26  38278  mblfinlem2  38290  cnambfre  38300  itgaddnclem2  38311  ftc1anclem1  38325  grpokerinj  38525  rngoisoval  38609  smprngopr  38684  parteq12  39509  ax12eq  39696  ax12el  39697  2llnjN  40322  2lplnj  40375  elpadd0  40564  lauteq  40850  lpolconN  42242  rexrabdioph  43504  tfsnfin  44062  eliunov2  44388  nzss  45010  iotasbc2  45113  or2expropbilem2  47753  elsetpreimafvbi  48123  reuopreuprim  48258  grlicref  48760  smprngprmrng  49087  cbvmpox2  49099  naryfvalel  49393  line2x  49517  brab2ddw  49590  brab2ddw2  49591