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  2837  eleq12  2904  sbhypf  3554  ceqsrex2v  3653  vtocl2dOLD  3933  sseq12  3996  csbie2df  4394  2ralsng  4618  rexprgf  4633  rextpg  4637  breq12  5073  reusv2lem5  5305  opelopabg  5427  brabg  5428  opelopabgf  5429  opelopab2  5430  rbropapd  5451  ralxpf  5719  feq23  6500  f00  6563  fconstg  6568  f1oeq23  6609  f1o00  6651  fnelfp  6939  fnelnfp  6941  isofrlem  7095  f1oiso  7106  riota1a  7138  cbvmpox  7249  caovord  7361  caovord3  7363  f1oweALT  7675  oaordex  8186  oaass  8189  odi  8207  findcard2s  8761  unfilem1  8784  suppeqfsuppbi  8849  oieu  9005  r1pw  9276  carddomi2  9401  isacn  9472  djudom2  9611  axdc2  9873  alephval2  9996  fpwwe2cbv  10054  fpwwe2lem2  10056  fpwwecbv  10068  fpwwelem  10069  canthwelem  10074  canthwe  10075  distrlem4pr  10450  axpre-sup  10593  nn0ind-raph  12085  elpq  12377  xnn0xadd0  12643  elfz  12901  elfzp12  12989  expeq0  13462  leiso  13820  wrd2ind  14087  trcleq12lem  14355  dfrtrclrec2  14418  shftfib  14433  absdvdsb  15630  dvdsabsb  15631  dvdsabseq  15665  unbenlem  16246  isprs  17542  isdrs  17546  pltval  17572  lublecllem  17600  istos  17647  isdlat  17805  znfld  20709  tgss2  21597  isopn2  21642  cnpf2  21860  lmbr  21868  isreg2  21987  fclsrest  22634  qustgplem  22731  ustuqtoplem  22850  xmetec  23046  nmogelb  23327  metdstri  23461  tcphcph  23842  ulmval  24970  2lgslem1a  25969  iscgrg  26300  istrlson  27490  ispthson  27525  isspthson  27526  elwwlks2on  27740  eupth2lem1  27999  eigrei  29613  eigorthi  29616  jplem1  30047  superpos  30133  chrelati  30143  br8d  30363  issiga  31373  eulerpartlemgvv  31636  cplgredgex  32369  acycgrcycl  32396  br8  32994  br6  32995  br4  32996  brsegle  33571  topfne  33704  tailfb  33727  filnetlem1  33728  nndivsub  33807  bj-elequ12  34014  bj-rest10  34381  isbasisrelowllem1  34638  isbasisrelowllem2  34639  fvineqsnf1  34693  wl-2sb6d  34796  curf  34872  curunc  34876  poimirlem26  34920  mblfinlem2  34932  cnambfre  34942  itgaddnclem2  34953  ftc1anclem1  34969  grpokerinj  35173  rngoisoval  35257  smprngopr  35332  ax12eq  36079  ax12el  36080  2llnjN  36705  2lplnj  36758  elpadd0  36947  lauteq  37233  lpolconN  38625  rexrabdioph  39398  eliunov2  40031  nzss  40656  iotasbc2  40759  or2expropbilem2  43275  elsetpreimafvbi  43558  reuopreuprim  43695  cbvmpox2  44391  line2x  44748