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  2502  2sb6rf  2503  eqeqan12d  2775  eleq12  2851  ceqsrex2v  3612  elabd2  3624  elabgt  3626  sseq12  3958  csbie2df  4401  2ralsng  4639  rexprgf  4656  rextpg  4660  breq12  5108  reusv2lem5  5364  opelopabg  5513  brabg  5514  opelopabgf  5515  opelopab2  5516  rbropapd  5537  poeq12d  5564  soeq12d  5582  freq12d  5620  seeq12d  5623  weeq12d  5640  ralxpf  5824  feq23  6688  f00  6762  fconstg  6767  f1oeq23  6813  f1o00  6858  fnelfp  7178  fnelnfp  7180  isofrlem  7346  f1oiso  7357  riota1a  7397  cbvmpox  7511  caovord  7630  caovord3  7632  f1oweALT  7982  mpof1o2d  8135  oaordex  8559  oaass  8562  odi  8580  curf  8883  findcard2s  9174  unfilem1  9290  tfsnfin2  9345  suppeqfsuppbi  9364  oieu  9526  r1pw  9852  carddomi2  10044  isacn  10116  djudom2  10255  axdc2  10520  alephval2  10650  distrlem4pr  11104  axpre-sup  11247  nn0ind-raph  12792  elpq  13096  xnn0xadd0  13370  elfz  13638  elfzp12  13730  expeq0  14228  leiso  14597  wrd2ind  14865  trcleq12lem  15139  dfrtrclrec2  15204  shftfib  15218  absdvdsb  16437  dvdsabsb  16438  dvdsabseq  16476  unbenlem  17079  isprs  18463  isdrs  18468  pltval  18497  lublecllem  18525  istos  18583  isdlat  18689  znfld  21859  tgss2  23298  isopn2  23343  cnpf2  23561  lmbr  23569  isreg2  23688  fclsrest  24336  qustgplem  24433  ustuqtoplem  24551  xmetec  24746  nmogelb  25028  metdstri  25164  tcphcph  25551  ulmval  26700  2lgslem1a  27711  elmade  28236  bdayle  28295  iscgrg  28968  istrlson  30282  ispthson  30321  isspthson  30322  elwwlks2on  30543  acycgrcycl  30746  eupth2lem1  30812  eigrei  32429  eigorthi  32432  jplem1  32863  superpos  32949  chrelati  32959  br8d  33195  ellpi  33921  issiga  34737  eulerpartlemgvv  35001  cplgredgex  35884  br8  36500  br6  36501  br4  36502  brsegle  36853  topfne  37122  tailfb  37145  filnetlem1  37146  nndivsub  37225  bj-rest10  37989  isbasisrelowllem1  38258  isbasisrelowllem2  38259  fvineqsnf1  38313  wl-2sb6d  38470  curunc  38505  poimirlem26  38544  mblfinlem2  38556  cnambfre  38566  itgaddnclem2  38577  ftc1anclem1  38591  grpokerinj  38807  rngoisoval  38891  smprngopr  38966  parteq12  39791  ax12eq  39978  ax12el  39979  2llnjN  40604  2lplnj  40657  elpadd0  40846  lauteq  41132  lpolconN  42524  rexrabdioph  43780  tfsnfin  44338  eliunov2  44664  nzss  45286  iotasbc2  45389  or2expropbilem2  48072  elsetpreimafvbi  48442  reuopreuprim  48577  grlicref  49079  smprngprmrng  49405  cbvmpox2  49417  naryfvalel  49711  line2x  49835  brab2ddw  49908  brab2ddw2  49909