Theorem sylan9bb 508

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 479	. 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜒))
3		sylan9bb.2	. . 3 ⊢ (𝜃 → (𝜒 ↔ 𝜏))
4	3	adantl 480	. 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜒 ↔ 𝜏))
5	2, 4	bitrd 278	1 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394

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 395

This theorem is referenced by:  sylan9bbr  509  baibd  538  syl3an9b  1432  nanbi12  1499  sbcom2  2159  2sb5rf  2469  2sb6rf  2470  eqeqan12d  2744  eqeq12OLD  2749  eleq12  2821  sbhypfOLD  3538  ceqsrex2v  3645  elabd2  3659  sseq12  4008  csbie2df  4439  2ralsng  4679  rexprgf  4696  rextpg  4702  breq12  5152  reusv2lem5  5399  opelopabg  5537  brabg  5538  opelopabgf  5539  opelopab2  5540  rbropapd  5563  ralxpf  5845  feq23  6700  f00  6772  fconstg  6777  f1oeq23  6823  f1o00  6867  fnelfp  7174  fnelnfp  7176  isofrlem  7339  f1oiso  7350  riota1a  7390  cbvmpox  7504  caovord  7620  caovord3  7622  f1oweALT  7961  oaordex  8560  oaass  8563  odi  8581  findcard2s  9167  unfilem1  9312  suppeqfsuppbi  9379  oieu  9536  r1pw  9842  carddomi2  9967  isacn  10041  djudom2  10180  axdc2  10446  alephval2  10569  fpwwe2cbv  10627  fpwwe2lem2  10629  fpwwecbv  10641  fpwwelem  10642  canthwelem  10647  canthwe  10648  distrlem4pr  11023  axpre-sup  11166  nn0ind-raph  12666  elpq  12963  xnn0xadd0  13230  elfz  13494  elfzp12  13584  expeq0  14062  leiso  14424  wrd2ind  14677  trcleq12lem  14944  dfrtrclrec2  15009  shftfib  15023  absdvdsb  16222  dvdsabsb  16223  dvdsabseq  16260  unbenlem  16845  isprs  18254  isdrs  18258  pltval  18289  lublecllem  18317  istos  18375  isdlat  18479  znfld  21335  tgss2  22710  isopn2  22756  cnpf2  22974  lmbr  22982  isreg2  23101  fclsrest  23748  qustgplem  23845  ustuqtoplem  23964  xmetec  24160  nmogelb  24453  metdstri  24587  tcphcph  24985  ulmval  26128  2lgslem1a  27130  elmade  27599  iscgrg  28030  istrlson  29231  ispthson  29266  isspthson  29267  elwwlks2on  29480  eupth2lem1  29738  eigrei  31354  eigorthi  31357  jplem1  31788  superpos  31874  chrelati  31884  br8d  32106  issiga  33408  eulerpartlemgvv  33673  cplgredgex  34409  acycgrcycl  34436  br8  35030  br6  35031  br4  35032  brsegle  35384  topfne  35542  tailfb  35565  filnetlem1  35566  nndivsub  35645  bj-elequ12  35859  bj-rest10  36272  isbasisrelowllem1  36539  isbasisrelowllem2  36540  fvineqsnf1  36594  wl-2sb6d  36726  curf  36769  curunc  36773  poimirlem26  36817  mblfinlem2  36829  cnambfre  36839  itgaddnclem2  36850  ftc1anclem1  36864  grpokerinj  37064  rngoisoval  37148  smprngopr  37223  parteq12  37949  ax12eq  38114  ax12el  38115  2llnjN  38741  2lplnj  38794  elpadd0  38983  lauteq  39269  lpolconN  40661  f1o2d2  41361  rexrabdioph  41834  tfsnfin  42404  eliunov2  42732  nzss  43378  iotasbc2  43481  or2expropbilem2  46041  elsetpreimafvbi  46357  reuopreuprim  46492  cbvmpox2  47099  naryfvalel  47403  line2x  47527