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  2163  sbcom2  2209  2sb5rf  2501  2sb6rf  2502  eqeqan12d  2774  eleq12  2850  ceqsrex2v  3612  elabd2  3624  elabgt  3626  sseq12  3958  csbie2df  4401  2ralsng  4639  rexprgf  4656  rextpg  4660  breq12  5108  reusv2lem5  5367  opelopabg  5517  brabg  5518  opelopabgf  5519  opelopab2  5520  rbropapd  5541  poeq12d  5568  soeq12d  5586  freq12d  5624  seeq12d  5627  weeq12d  5644  ralxpf  5826  feq23  6683  f00  6757  fconstg  6762  f1oeq23  6808  f1o00  6853  fnelfp  7173  fnelnfp  7175  isofrlem  7341  f1oiso  7352  riota1a  7392  cbvmpox  7506  caovord  7625  caovord3  7627  f1oweALT  7969  mpof1o2d  8123  oaordex  8545  oaass  8548  odi  8566  curf  8869  findcard2s  9160  unfilem1  9275  tfsnfin2  9330  suppeqfsuppbi  9349  oieu  9511  r1pw  9827  carddomi2  9975  isacn  10047  djudom2  10186  axdc2  10451  alephval2  10581  distrlem4pr  11035  axpre-sup  11178  nn0ind-raph  12721  elpq  13025  xnn0xadd0  13299  elfz  13567  elfzp12  13658  expeq0  14156  leiso  14524  wrd2ind  14792  trcleq12lem  15066  dfrtrclrec2  15131  shftfib  15145  absdvdsb  16364  dvdsabsb  16365  dvdsabseq  16403  unbenlem  17000  isprs  18384  isdrs  18389  pltval  18418  lublecllem  18446  istos  18504  isdlat  18610  znfld  21773  tgss2  23212  isopn2  23257  cnpf2  23475  lmbr  23483  isreg2  23602  fclsrest  24250  qustgplem  24347  ustuqtoplem  24465  xmetec  24660  nmogelb  24942  metdstri  25078  tcphcph  25465  ulmval  26616  2lgslem1a  27627  elmade  28122  bdayle  28181  iscgrg  28854  istrlson  30168  ispthson  30207  isspthson  30208  elwwlks2on  30429  acycgrcycl  30632  eupth2lem1  30698  eigrei  32315  eigorthi  32318  jplem1  32749  superpos  32835  chrelati  32845  br8d  33081  ellpi  33807  issiga  34622  eulerpartlemgvv  34887  cplgredgex  35719  br8  36335  br6  36336  br4  36337  brsegle  36688  topfne  36973  tailfb  36996  filnetlem1  36997  nndivsub  37076  bj-rest10  37838  isbasisrelowllem1  38109  isbasisrelowllem2  38110  fvineqsnf1  38164  wl-2sb6d  38321  curunc  38356  poimirlem26  38395  mblfinlem2  38407  cnambfre  38417  itgaddnclem2  38428  ftc1anclem1  38442  grpokerinj  38643  rngoisoval  38727  smprngopr  38802  parteq12  39627  ax12eq  39814  ax12el  39815  2llnjN  40440  2lplnj  40493  elpadd0  40682  lauteq  40968  lpolconN  42360  rexrabdioph  43635  tfsnfin  44193  eliunov2  44519  nzss  45141  iotasbc2  45244  or2expropbilem2  47921  elsetpreimafvbi  48291  reuopreuprim  48426  grlicref  48928  smprngprmrng  49254  cbvmpox2  49266  naryfvalel  49560  line2x  49684  brab2ddw  49757  brab2ddw2  49758