Theorem sylan9bb 512

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  sylan9bbr  513  baibd  542  syl3an9b  1430  nanbi12  1493  sbcom2  2168  2sb5rf  2496  2sb6rf  2497  eqeq12  2835  eleq12  2902  sbhypf  3552  ceqsrex2v  3651  vtocl2dOLD  3931  sseq12  3994  csbie2df  4392  2ralsng  4616  rexprgf  4631  rextpg  4635  breq12  5071  reusv2lem5  5303  opelopabg  5425  brabg  5426  opelopabgf  5427  opelopab2  5428  rbropapd  5449  ralxpf  5717  feq23  6498  f00  6561  fconstg  6566  f1oeq23  6607  f1o00  6649  fnelfp  6937  fnelnfp  6939  isofrlem  7093  f1oiso  7104  riota1a  7136  cbvmpox  7247  caovord  7359  caovord3  7361  f1oweALT  7673  oaordex  8184  oaass  8187  odi  8205  findcard2s  8759  unfilem1  8782  suppeqfsuppbi  8847  oieu  9003  r1pw  9274  carddomi2  9399  isacn  9470  djudom2  9609  axdc2  9871  alephval2  9994  fpwwe2cbv  10052  fpwwe2lem2  10054  fpwwecbv  10066  fpwwelem  10067  canthwelem  10072  canthwe  10073  distrlem4pr  10448  axpre-sup  10591  nn0ind-raph  12083  elpq  12375  xnn0xadd0  12641  elfz  12899  elfzp12  12987  expeq0  13460  leiso  13818  wrd2ind  14085  trcleq12lem  14353  dfrtrclrec2  14416  shftfib  14431  absdvdsb  15628  dvdsabsb  15629  dvdsabseq  15663  unbenlem  16244  isprs  17540  isdrs  17544  pltval  17570  lublecllem  17598  istos  17645  isdlat  17803  znfld  20707  tgss2  21595  isopn2  21640  cnpf2  21858  lmbr  21866  isreg2  21985  fclsrest  22632  qustgplem  22729  ustuqtoplem  22848  xmetec  23044  nmogelb  23325  metdstri  23459  tcphcph  23840  ulmval  24968  2lgslem1a  25967  iscgrg  26298  istrlson  27488  ispthson  27523  isspthson  27524  elwwlks2on  27738  eupth2lem1  27997  eigrei  29611  eigorthi  29614  jplem1  30045  superpos  30131  chrelati  30141  br8d  30361  issiga  31371  eulerpartlemgvv  31634  cplgredgex  32367  acycgrcycl  32394  br8  32992  br6  32993  br4  32994  brsegle  33569  topfne  33702  tailfb  33725  filnetlem1  33726  nndivsub  33805  bj-elequ12  34012  bj-rest10  34382  isbasisrelowllem1  34639  isbasisrelowllem2  34640  fvineqsnf1  34694  wl-2sb6d  34809  curf  34885  curunc  34889  poimirlem26  34933  mblfinlem2  34945  cnambfre  34955  itgaddnclem2  34966  ftc1anclem1  34982  grpokerinj  35186  rngoisoval  35270  smprngopr  35345  ax12eq  36092  ax12el  36093  2llnjN  36718  2lplnj  36771  elpadd0  36960  lauteq  37246  lpolconN  38638  rexrabdioph  39411  eliunov2  40044  nzss  40669  iotasbc2  40772  or2expropbilem2  43288  elsetpreimafvbi  43571  reuopreuprim  43708  cbvmpox2  44404  line2x  44761