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  1503  elequ12  2127  sbcom2  2174  2sb5rf  2470  2sb6rf  2471  eqeqan12d  2743  eleq12  2818  sbhypfOLD  3508  ceqsrex2v  3621  elabd2  3633  elabgt  3635  sseq12  3971  csbie2df  4402  2ralsng  4638  rexprgf  4655  rextpg  4659  breq12  5107  reusv2lem5  5352  opelopabg  5493  brabg  5494  opelopabgf  5495  opelopab2  5496  rbropapd  5517  poeq12d  5544  soeq12d  5562  freq12d  5600  seeq12d  5603  weeq12d  5620  ralxpf  5800  feq23  6651  f00  6724  fconstg  6729  f1oeq23  6773  f1o00  6817  fnelfp  7131  fnelnfp  7133  isofrlem  7297  f1oiso  7308  riota1a  7348  cbvmpox  7462  caovord  7580  caovord3  7582  f1oweALT  7930  oaordex  8499  oaass  8502  odi  8520  findcard2s  9106  unfilem1  9230  suppeqfsuppbi  9306  oieu  9468  r1pw  9774  carddomi2  9899  isacn  9973  djudom2  10113  axdc2  10378  alephval2  10501  distrlem4pr  10955  axpre-sup  11098  nn0ind-raph  12610  elpq  12910  xnn0xadd0  13183  elfz  13450  elfzp12  13540  expeq0  14033  leiso  14400  wrd2ind  14664  trcleq12lem  14935  dfrtrclrec2  15000  shftfib  15014  absdvdsb  16220  dvdsabsb  16221  dvdsabseq  16259  unbenlem  16855  isprs  18233  isdrs  18238  pltval  18267  lublecllem  18295  istos  18353  isdlat  18457  znfld  21446  tgss2  22850  isopn2  22895  cnpf2  23113  lmbr  23121  isreg2  23240  fclsrest  23887  qustgplem  23984  ustuqtoplem  24103  xmetec  24298  nmogelb  24580  metdstri  24716  tcphcph  25113  ulmval  26265  2lgslem1a  27278  elmade  27755  iscgrg  28415  istrlson  29608  ispthson  29645  isspthson  29646  elwwlks2on  29862  eupth2lem1  30120  eigrei  31736  eigorthi  31739  jplem1  32170  superpos  32256  chrelati  32266  bian1d  32358  br8d  32511  ellpi  33317  issiga  34075  eulerpartlemgvv  34340  cplgredgex  35081  acycgrcycl  35107  br8  35716  br6  35717  br4  35718  brsegle  36069  topfne  36315  tailfb  36338  filnetlem1  36339  nndivsub  36418  bj-rest10  37049  isbasisrelowllem1  37316  isbasisrelowllem2  37317  fvineqsnf1  37371  wl-2sb6d  37519  curf  37565  curunc  37569  poimirlem26  37613  mblfinlem2  37625  cnambfre  37635  itgaddnclem2  37646  ftc1anclem1  37660  grpokerinj  37860  rngoisoval  37944  smprngopr  38019  parteq12  38741  ax12eq  38907  ax12el  38908  2llnjN  39534  2lplnj  39587  elpadd0  39776  lauteq  40062  lpolconN  41454  f1o2d2  42194  rexrabdioph  42755  tfsnfin  43314  eliunov2  43641  nzss  44279  iotasbc2  44382  or2expropbilem2  47007  elsetpreimafvbi  47365  reuopreuprim  47500  grlicref  47977  cbvmpox2  48297  naryfvalel  48592  line2x  48716  brab2ddw  48790  brab2ddw2  48791