Theorem sylan9bb 519

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  sylan9bbr  520  baibd  549  syl3an9b  1462  nanbi12  1532  elequ12  2162  sbcom2  2208  2sb5rf  2501  2sb6rf  2502  eqeqan12d  2774  eleq12  2850  ceqsrex2v  3611  elabd2  3623  elabgt  3625  sseq12  3935  csbie2df  4400  2ralsng  4635  rexprgf  4652  rextpg  4656  breq12  5107  reusv2lem5  5363  opelopabg  5512  brabg  5513  opelopabgf  5514  opelopab2  5515  rbropapd  5536  poeq12d  5563  soeq12d  5581  freq12d  5619  seeq12d  5622  weeq12d  5639  ralxpf  5823  feq23  6691  f00  6765  fconstg  6770  f1oeq23  6816  f1o00  6861  fnelfp  7181  fnelnfp  7183  isofrlem  7349  f1oiso  7360  riota1a  7400  cbvmpox  7514  caovord  7633  caovord3  7635  f1oweALT  7985  mpof1o2d  8140  oaordex  8570  oaass  8573  odi  8591  curf  8894  findcard2s  9185  unfilem1  9301  tfsnfin2  9356  suppeqfsuppbi  9375  oieu  9537  r1pw  9863  carddomi2  10055  isacn  10127  djudom2  10266  axdc2  10531  alephval2  10661  distrlem4pr  11115  axpre-sup  11258  nn0ind-raph  12803  elpq  13107  xnn0xadd0  13381  elfz  13649  elfzp12  13741  expeq0  14239  leiso  14608  wrd2ind  14877  trcleq12lem  15152  dfrtrclrec2  15217  shftfib  15231  absdvdsb  16450  dvdsabsb  16451  dvdsabseq  16489  unbenlem  17092  isprs  18476  isdrs  18481  pltval  18510  lublecllem  18538  istos  18596  isdlat  18702  znfld  21872  tgss2  23311  isopn2  23356  cnpf2  23574  lmbr  23582  isreg2  23701  fclsrest  24349  qustgplem  24446  ustuqtoplem  24564  xmetec  24759  nmogelb  25041  metdstri  25177  tcphcph  25564  ulmval  26713  2lgslem1a  27724  elmade  28249  bdayle  28308  iscgrg  28981  istrlson  30295  ispthson  30334  isspthson  30335  elwwlks2on  30556  acycgrcycl  30759  eupth2lem1  30825  eigrei  32442  eigorthi  32445  jplem1  32876  superpos  32962  chrelati  32972  br8d  33250  ellpi  33975  issiga  34791  eulerpartlemgvv  35055  cplgredgex  35982  br8  36614  br6  36615  br4  36616  brsegle  36966  topfne  37235  tailfb  37258  filnetlem1  37259  nndivsub  37338  bj-rest10  38102  isbasisrelowllem1  38372  isbasisrelowllem2  38373  fvineqsnf1  38427  wl-2sb6d  38584  curunc  38619  poimirlem26  38658  mblfinlem2  38670  cnambfre  38680  itgaddnclem2  38691  ftc1anclem1  38705  grpokerinj  38921  rngoisoval  39005  smprngopr  39080  parteq12  39905  ax12eq  40092  ax12el  40093  2llnjN  40718  2lplnj  40771  elpadd0  40960  lauteq  41246  lpolconN  42638  rexrabdioph  43895  tfsnfin  44448  eliunov2  44773  nzss  45395  iotasbc2  45498  or2expropbilem2  48197  elsetpreimafvbi  48567  reuopreuprim  48702  grlicref  49204  smprngprmrng  49530  cbvmpox2  49542  naryfvalel  49836  line2x  49960  brab2ddw  50034  brab2ddw2  50035