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  1437  nanbi12  1505  elequ12  2132  sbcom2  2179  2sb5rf  2476  2sb6rf  2477  eqeqan12d  2750  eleq12  2826  ceqsrex2v  3600  elabd2  3612  elabgt  3614  sseq12  3949  csbie2df  4383  2ralsng  4622  rexprgf  4639  rextpg  4643  breq12  5090  reusv2lem5  5344  opelopabg  5493  brabg  5494  opelopabgf  5495  opelopab2  5496  rbropapd  5517  poeq12d  5544  soeq12d  5562  freq12d  5600  seeq12d  5603  weeq12d  5620  ralxpf  5801  feq23  6649  f00  6722  fconstg  6727  f1oeq23  6771  f1o00  6815  fnelfp  7130  fnelnfp  7132  isofrlem  7295  f1oiso  7306  riota1a  7346  cbvmpox  7460  caovord  7578  caovord3  7580  f1oweALT  7925  oaordex  8493  oaass  8496  odi  8514  findcard2s  9100  unfilem1  9215  tfsnfin2  9273  suppeqfsuppbi  9292  oieu  9454  r1pw  9769  carddomi2  9894  isacn  9966  djudom2  10106  axdc2  10371  alephval2  10495  distrlem4pr  10949  axpre-sup  11092  nn0ind-raph  12629  elpq  12925  xnn0xadd0  13199  elfz  13467  elfzp12  13557  expeq0  14054  leiso  14421  wrd2ind  14685  trcleq12lem  14955  dfrtrclrec2  15020  shftfib  15034  absdvdsb  16243  dvdsabsb  16244  dvdsabseq  16282  unbenlem  16879  isprs  18262  isdrs  18267  pltval  18296  lublecllem  18324  istos  18382  isdlat  18488  znfld  21540  tgss2  22952  isopn2  22997  cnpf2  23215  lmbr  23223  isreg2  23342  fclsrest  23989  qustgplem  24086  ustuqtoplem  24204  xmetec  24399  nmogelb  24681  metdstri  24817  tcphcph  25204  ulmval  26345  2lgslem1a  27354  elmade  27849  bdayle  27908  iscgrg  28580  istrlson  29773  ispthson  29810  isspthson  29811  elwwlks2on  30029  eupth2lem1  30288  eigrei  31905  eigorthi  31908  jplem1  32339  superpos  32425  chrelati  32435  br8d  32681  ellpi  33433  issiga  34256  eulerpartlemgvv  34520  cplgredgex  35303  acycgrcycl  35329  br8  35938  br6  35939  br4  35940  brsegle  36290  topfne  36536  tailfb  36559  filnetlem1  36560  nndivsub  36639  bj-rest10  37400  isbasisrelowllem1  37671  isbasisrelowllem2  37672  fvineqsnf1  37726  wl-2sb6d  37883  curf  37919  curunc  37923  poimirlem26  37967  mblfinlem2  37979  cnambfre  37989  itgaddnclem2  38000  ftc1anclem1  38014  grpokerinj  38214  rngoisoval  38298  smprngopr  38373  parteq12  39200  ax12eq  39387  ax12el  39388  2llnjN  40013  2lplnj  40066  elpadd0  40255  lauteq  40541  lpolconN  41933  f1o2d2  42674  rexrabdioph  43222  tfsnfin  43780  eliunov2  44106  nzss  44744  iotasbc2  44847  or2expropbilem2  47481  elsetpreimafvbi  47851  reuopreuprim  47986  grlicref  48488  cbvmpox2  48812  naryfvalel  49106  line2x  49230  brab2ddw  49304  brab2ddw2  49305