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  1432  nanbi12  1495  sbcom2  2163  2sb5rf  2472  2sb6rf  2473  eqeqan12d  2752  eqeq12OLD  2757  eleq12  2828  sbhypf  3481  ceqsrex2v  3580  elabd2  3594  sseq12  3944  csbie2df  4371  2ralsng  4609  rexprgf  4626  rextpg  4632  breq12  5075  reusv2lem5  5320  opelopabg  5444  brabg  5445  opelopabgf  5446  opelopab2  5447  rbropapd  5468  ralxpf  5744  feq23  6568  f00  6640  fconstg  6645  f1oeq23  6691  f1o00  6734  fnelfp  7029  fnelnfp  7031  isofrlem  7191  f1oiso  7202  riota1a  7235  cbvmpox  7346  caovord  7461  caovord3  7463  f1oweALT  7788  oaordex  8351  oaass  8354  odi  8372  findcard2s  8910  unfilem1  9008  suppeqfsuppbi  9072  oieu  9228  r1pw  9534  carddomi2  9659  isacn  9731  djudom2  9870  axdc2  10136  alephval2  10259  fpwwe2cbv  10317  fpwwe2lem2  10319  fpwwecbv  10331  fpwwelem  10332  canthwelem  10337  canthwe  10338  distrlem4pr  10713  axpre-sup  10856  nn0ind-raph  12350  elpq  12644  xnn0xadd0  12910  elfz  13174  elfzp12  13264  expeq0  13741  leiso  14101  wrd2ind  14364  trcleq12lem  14632  dfrtrclrec2  14697  shftfib  14711  absdvdsb  15912  dvdsabsb  15913  dvdsabseq  15950  unbenlem  16537  isprs  17930  isdrs  17934  pltval  17965  lublecllem  17993  istos  18051  isdlat  18155  znfld  20680  tgss2  22045  isopn2  22091  cnpf2  22309  lmbr  22317  isreg2  22436  fclsrest  23083  qustgplem  23180  ustuqtoplem  23299  xmetec  23495  nmogelb  23786  metdstri  23920  tcphcph  24306  ulmval  25444  2lgslem1a  26444  iscgrg  26777  istrlson  27976  ispthson  28011  isspthson  28012  elwwlks2on  28225  eupth2lem1  28483  eigrei  30097  eigorthi  30100  jplem1  30531  superpos  30617  chrelati  30627  br8d  30851  issiga  31980  eulerpartlemgvv  32243  cplgredgex  32982  acycgrcycl  33009  br8  33629  br6  33630  br4  33631  elmade  33978  brsegle  34337  topfne  34470  tailfb  34493  filnetlem1  34494  nndivsub  34573  bj-elequ12  34787  bj-rest10  35186  isbasisrelowllem1  35453  isbasisrelowllem2  35454  fvineqsnf1  35508  wl-2sb6d  35640  curf  35682  curunc  35686  poimirlem26  35730  mblfinlem2  35742  cnambfre  35752  itgaddnclem2  35763  ftc1anclem1  35777  grpokerinj  35978  rngoisoval  36062  smprngopr  36137  ax12eq  36882  ax12el  36883  2llnjN  37508  2lplnj  37561  elpadd0  37750  lauteq  38036  lpolconN  39428  rexrabdioph  40532  eliunov2  41176  nzss  41824  iotasbc2  41927  or2expropbilem2  44414  elsetpreimafvbi  44731  reuopreuprim  44866  cbvmpox2  45559  naryfvalel  45864  line2x  45988