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  2477  2sb6rf  2478  eqeqan12d  2750  eleq12  2825  sbhypfOLD  3529  ceqsrex2v  3642  elabd2  3654  sseq12  3991  csbie2df  4423  2ralsng  4659  rexprgf  4676  rextpg  4680  breq12  5129  reusv2lem5  5377  opelopabg  5518  brabg  5519  opelopabgf  5520  opelopab2  5521  rbropapd  5544  poeq12d  5571  soeq12d  5589  freq12d  5628  seeq12d  5631  weeq12d  5648  ralxpf  5831  feq23  6694  f00  6765  fconstg  6770  f1oeq23  6814  f1o00  6858  fnelfp  7172  fnelnfp  7174  isofrlem  7338  f1oiso  7349  riota1a  7389  cbvmpox  7505  caovord  7623  caovord3  7625  f1oweALT  7976  oaordex  8575  oaass  8578  odi  8596  findcard2s  9184  unfilem1  9320  suppeqfsuppbi  9396  oieu  9558  r1pw  9864  carddomi2  9989  isacn  10063  djudom2  10203  axdc2  10468  alephval2  10591  distrlem4pr  11045  axpre-sup  11188  nn0ind-raph  12698  elpq  12996  xnn0xadd0  13268  elfz  13535  elfzp12  13625  expeq0  14115  leiso  14482  wrd2ind  14746  trcleq12lem  15017  dfrtrclrec2  15082  shftfib  15096  absdvdsb  16299  dvdsabsb  16300  dvdsabseq  16337  unbenlem  16933  isprs  18313  isdrs  18318  pltval  18347  lublecllem  18375  istos  18433  isdlat  18537  znfld  21526  tgss2  22930  isopn2  22975  cnpf2  23193  lmbr  23201  isreg2  23320  fclsrest  23967  qustgplem  24064  ustuqtoplem  24183  xmetec  24378  nmogelb  24660  metdstri  24796  tcphcph  25194  ulmval  26346  2lgslem1a  27359  elmade  27836  iscgrg  28496  istrlson  29692  ispthson  29729  isspthson  29730  elwwlks2on  29946  eupth2lem1  30204  eigrei  31820  eigorthi  31823  jplem1  32254  superpos  32340  chrelati  32350  bian1d  32442  br8d  32595  ellpi  33393  issiga  34148  eulerpartlemgvv  34413  cplgredgex  35148  acycgrcycl  35174  br8  35778  br6  35779  br4  35780  brsegle  36131  topfne  36377  tailfb  36400  filnetlem1  36401  nndivsub  36480  bj-rest10  37111  isbasisrelowllem1  37378  isbasisrelowllem2  37379  fvineqsnf1  37433  wl-2sb6d  37581  curf  37627  curunc  37631  poimirlem26  37675  mblfinlem2  37687  cnambfre  37697  itgaddnclem2  37708  ftc1anclem1  37722  grpokerinj  37922  rngoisoval  38006  smprngopr  38081  parteq12  38799  ax12eq  38964  ax12el  38965  2llnjN  39591  2lplnj  39644  elpadd0  39833  lauteq  40119  lpolconN  41511  f1o2d2  42251  rexrabdioph  42792  tfsnfin  43351  eliunov2  43678  nzss  44316  iotasbc2  44419  or2expropbilem2  47042  elsetpreimafvbi  47385  reuopreuprim  47520  grlicref  47997  cbvmpox2  48291  naryfvalel  48590  line2x  48714  brab2ddw  48787  brab2ddw2  48788