Theorem sylan9bb 519

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  sylan9bbr  520  baibd  549  syl3an9b  1462  nanbi12  1533  elequ12  2164  sbcom2  2210  2sb5rf  2506  2sb6rf  2507  eqeqan12d  2779  eleq12  2855  ceqsrex2v  3619  elabd2  3631  elabgt  3633  sseq12  3965  csbie2df  4408  2ralsng  4646  rexprgf  4663  rextpg  4667  breq12  5116  reusv2lem5  5375  opelopabg  5525  brabg  5526  opelopabgf  5527  opelopab2  5528  rbropapd  5549  poeq12d  5576  soeq12d  5594  freq12d  5632  seeq12d  5635  weeq12d  5652  ralxpf  5834  feq23  6690  f00  6764  fconstg  6769  f1oeq23  6815  f1o00  6860  fnelfp  7177  fnelnfp  7179  isofrlem  7344  f1oiso  7355  riota1a  7395  cbvmpox  7509  caovord  7627  caovord3  7629  f1oweALT  7971  mpof1o2d  8123  oaordex  8545  oaass  8548  odi  8566  findcard2s  9153  unfilem1  9268  tfsnfin2  9323  suppeqfsuppbi  9342  oieu  9504  r1pw  9820  carddomi2  9968  isacn  10040  djudom2  10179  axdc2  10444  alephval2  10568  distrlem4pr  11022  axpre-sup  11165  nn0ind-raph  12707  elpq  13010  xnn0xadd0  13284  elfz  13552  elfzp12  13643  expeq0  14141  leiso  14509  wrd2ind  14777  trcleq12lem  15049  dfrtrclrec2  15114  shftfib  15128  absdvdsb  16349  dvdsabsb  16350  dvdsabseq  16388  unbenlem  16985  isprs  18369  isdrs  18374  pltval  18403  lublecllem  18431  istos  18489  isdlat  18595  znfld  21739  tgss2  23173  isopn2  23218  cnpf2  23436  lmbr  23444  isreg2  23563  fclsrest  24210  qustgplem  24307  ustuqtoplem  24425  xmetec  24620  nmogelb  24902  metdstri  25038  tcphcph  25425  ulmval  26572  2lgslem1a  27584  elmade  28079  bdayle  28138  iscgrg  28810  istrlson  30083  ispthson  30120  isspthson  30121  elwwlks2on  30339  eupth2lem1  30598  eigrei  32215  eigorthi  32218  jplem1  32649  superpos  32735  chrelati  32745  br8d  32982  ellpi  33710  issiga  34525  eulerpartlemgvv  34790  cplgredgex  35626  acycgrcycl  35652  br8  36261  br6  36262  br4  36263  brsegle  36613  topfne  36898  tailfb  36921  filnetlem1  36922  nndivsub  37001  bj-rest10  37763  isbasisrelowllem1  38034  isbasisrelowllem2  38035  fvineqsnf1  38089  wl-2sb6d  38246  curf  38282  curunc  38286  poimirlem26  38330  mblfinlem2  38342  cnambfre  38352  itgaddnclem2  38363  ftc1anclem1  38377  grpokerinj  38577  rngoisoval  38661  smprngopr  38736  parteq12  39561  ax12eq  39748  ax12el  39749  2llnjN  40374  2lplnj  40427  elpadd0  40616  lauteq  40902  lpolconN  42294  rexrabdioph  43554  tfsnfin  44112  eliunov2  44438  nzss  45060  iotasbc2  45163  or2expropbilem2  47803  elsetpreimafvbi  48173  reuopreuprim  48308  grlicref  48810  smprngprmrng  49137  cbvmpox2  49149  naryfvalel  49443  line2x  49567  brab2ddw  49640  brab2ddw2  49641