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  1504  elequ12  2131  sbcom2  2178  2sb5rf  2474  2sb6rf  2475  eqeqan12d  2747  eleq12  2823  ceqsrex2v  3609  elabd2  3621  elabgt  3623  sseq12  3958  csbie2df  4392  2ralsng  4632  rexprgf  4649  rextpg  4653  breq12  5100  reusv2lem5  5344  opelopabg  5483  brabg  5484  opelopabgf  5485  opelopab2  5486  rbropapd  5507  poeq12d  5534  soeq12d  5552  freq12d  5590  seeq12d  5593  weeq12d  5610  ralxpf  5792  feq23  6640  f00  6713  fconstg  6718  f1oeq23  6762  f1o00  6806  fnelfp  7118  fnelnfp  7120  isofrlem  7283  f1oiso  7294  riota1a  7334  cbvmpox  7448  caovord  7566  caovord3  7568  f1oweALT  7913  oaordex  8482  oaass  8485  odi  8503  findcard2s  9086  unfilem1  9200  suppeqfsuppbi  9274  oieu  9436  r1pw  9749  carddomi2  9874  isacn  9946  djudom2  10086  axdc2  10351  alephval2  10474  distrlem4pr  10928  axpre-sup  11071  nn0ind-raph  12583  elpq  12879  xnn0xadd0  13153  elfz  13420  elfzp12  13510  expeq0  14006  leiso  14373  wrd2ind  14637  trcleq12lem  14907  dfrtrclrec2  14972  shftfib  14986  absdvdsb  16192  dvdsabsb  16193  dvdsabseq  16231  unbenlem  16827  isprs  18210  isdrs  18215  pltval  18244  lublecllem  18272  istos  18330  isdlat  18436  znfld  21506  tgss2  22922  isopn2  22967  cnpf2  23185  lmbr  23193  isreg2  23312  fclsrest  23959  qustgplem  24056  ustuqtoplem  24174  xmetec  24369  nmogelb  24651  metdstri  24787  tcphcph  25184  ulmval  26336  2lgslem1a  27349  elmade  27832  bdayle  27881  iscgrg  28510  istrlson  29704  ispthson  29741  isspthson  29742  elwwlks2on  29960  eupth2lem1  30219  eigrei  31835  eigorthi  31838  jplem1  32269  superpos  32355  chrelati  32365  bian1d  32456  br8d  32612  ellpi  33382  issiga  34197  eulerpartlemgvv  34461  cplgredgex  35237  acycgrcycl  35263  br8  35872  br6  35873  br4  35874  brsegle  36224  topfne  36470  tailfb  36493  filnetlem1  36494  nndivsub  36573  bj-rest10  37205  isbasisrelowllem1  37472  isbasisrelowllem2  37473  fvineqsnf1  37527  wl-2sb6d  37675  curf  37711  curunc  37715  poimirlem26  37759  mblfinlem2  37771  cnambfre  37781  itgaddnclem2  37792  ftc1anclem1  37806  grpokerinj  38006  rngoisoval  38090  smprngopr  38165  parteq12  38947  ax12eq  39113  ax12el  39114  2llnjN  39739  2lplnj  39792  elpadd0  39981  lauteq  40267  lpolconN  41659  f1o2d2  42404  rexrabdioph  42951  tfsnfin  43509  eliunov2  43836  nzss  44474  iotasbc2  44577  or2expropbilem2  47195  elsetpreimafvbi  47553  reuopreuprim  47688  grlicref  48174  cbvmpox2  48498  naryfvalel  48792  line2x  48916  brab2ddw  48990  brab2ddw2  48991