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 278	1 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  sylan9bbr  510  baibd  539  syl3an9b  1433  nanbi12  1500  sbcom2  2160  2sb5rf  2470  2sb6rf  2471  eqeqan12d  2745  eqeq12OLD  2750  eleq12  2822  sbhypfOLD  3539  ceqsrex2v  3647  elabd2  3661  sseq12  4010  csbie2df  4441  2ralsng  4681  rexprgf  4698  rextpg  4704  breq12  5154  reusv2lem5  5401  opelopabg  5539  brabg  5540  opelopabgf  5541  opelopab2  5542  rbropapd  5565  ralxpf  5847  feq23  6702  f00  6774  fconstg  6779  f1oeq23  6825  f1o00  6869  fnelfp  7176  fnelnfp  7178  isofrlem  7340  f1oiso  7351  riota1a  7391  cbvmpox  7505  caovord  7621  caovord3  7623  f1oweALT  7962  oaordex  8561  oaass  8564  odi  8582  findcard2s  9168  unfilem1  9313  suppeqfsuppbi  9380  oieu  9537  r1pw  9843  carddomi2  9968  isacn  10042  djudom2  10181  axdc2  10447  alephval2  10570  fpwwe2cbv  10628  fpwwe2lem2  10630  fpwwecbv  10642  fpwwelem  10643  canthwelem  10648  canthwe  10649  distrlem4pr  11024  axpre-sup  11167  nn0ind-raph  12667  elpq  12964  xnn0xadd0  13231  elfz  13495  elfzp12  13585  expeq0  14063  leiso  14425  wrd2ind  14678  trcleq12lem  14945  dfrtrclrec2  15010  shftfib  15024  absdvdsb  16223  dvdsabsb  16224  dvdsabseq  16261  unbenlem  16846  isprs  18255  isdrs  18259  pltval  18290  lublecllem  18318  istos  18376  isdlat  18480  znfld  21336  tgss2  22711  isopn2  22757  cnpf2  22975  lmbr  22983  isreg2  23102  fclsrest  23749  qustgplem  23846  ustuqtoplem  23965  xmetec  24161  nmogelb  24454  metdstri  24588  tcphcph  24986  ulmval  26125  2lgslem1a  27127  elmade  27596  iscgrg  28027  istrlson  29228  ispthson  29263  isspthson  29264  elwwlks2on  29477  eupth2lem1  29735  eigrei  31351  eigorthi  31354  jplem1  31785  superpos  31871  chrelati  31881  br8d  32103  issiga  33405  eulerpartlemgvv  33670  cplgredgex  34406  acycgrcycl  34433  br8  35027  br6  35028  br4  35029  brsegle  35381  topfne  35543  tailfb  35566  filnetlem1  35567  nndivsub  35646  bj-elequ12  35860  bj-rest10  36273  isbasisrelowllem1  36540  isbasisrelowllem2  36541  fvineqsnf1  36595  wl-2sb6d  36727  curf  36770  curunc  36774  poimirlem26  36818  mblfinlem2  36830  cnambfre  36840  itgaddnclem2  36851  ftc1anclem1  36865  grpokerinj  37065  rngoisoval  37149  smprngopr  37224  parteq12  37950  ax12eq  38115  ax12el  38116  2llnjN  38742  2lplnj  38795  elpadd0  38984  lauteq  39270  lpolconN  40662  f1o2d2  41362  rexrabdioph  41835  tfsnfin  42405  eliunov2  42733  nzss  43379  iotasbc2  43482  or2expropbilem2  46043  elsetpreimafvbi  46359  reuopreuprim  46494  cbvmpox2  47101  naryfvalel  47405  line2x  47529