Theorem sylan9bb 517

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399

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 400

This theorem is referenced by:  sylan9bbr  518  baibd  547  syl3an9b  1454  nanbi12  1522  elequ12  2159  sbcom2  2205  2sb5rf  2502  2sb6rf  2503  eqeqan12d  2775  eleq12  2851  ceqsrex2v  3616  elabd2  3628  elabgt  3630  sseq12  3961  csbie2df  4394  2ralsng  4634  rexprgf  4651  rextpg  4655  breq12  5102  reusv2lem5  5356  opelopabg  5505  brabg  5506  opelopabgf  5507  opelopab2  5508  rbropapd  5529  poeq12d  5556  soeq12d  5574  freq12d  5612  seeq12d  5615  weeq12d  5632  ralxpf  5814  feq23  6667  f00  6741  fconstg  6746  f1oeq23  6792  f1o00  6837  fnelfp  7154  fnelnfp  7156  isofrlem  7319  f1oiso  7330  riota1a  7370  cbvmpox  7484  caovord  7602  caovord3  7604  f1oweALT  7948  mpof1o2d  8099  oaordex  8521  oaass  8524  odi  8542  findcard2s  9128  unfilem1  9243  tfsnfin2  9300  suppeqfsuppbi  9319  oieu  9481  r1pw  9797  carddomi2  9922  isacn  9994  djudom2  10134  axdc2  10400  alephval2  10524  distrlem4pr  10978  axpre-sup  11121  nn0ind-raph  12667  elpq  12970  xnn0xadd0  13244  elfz  13512  elfzp12  13602  expeq0  14099  leiso  14466  wrd2ind  14730  trcleq12lem  15000  dfrtrclrec2  15065  shftfib  15079  absdvdsb  16299  dvdsabsb  16300  dvdsabseq  16338  unbenlem  16935  isprs  18319  isdrs  18324  pltval  18353  lublecllem  18381  istos  18439  isdlat  18545  znfld  21600  tgss2  23035  isopn2  23080  cnpf2  23298  lmbr  23306  isreg2  23425  fclsrest  24072  qustgplem  24169  ustuqtoplem  24287  xmetec  24482  nmogelb  24764  metdstri  24900  tcphcph  25287  ulmval  26431  2lgslem1a  27443  elmade  27938  bdayle  27997  iscgrg  28669  istrlson  29862  ispthson  29899  isspthson  29900  elwwlks2on  30118  eupth2lem1  30377  eigrei  31994  eigorthi  31997  jplem1  32428  superpos  32514  chrelati  32524  br8d  32771  ellpi  33520  issiga  34370  eulerpartlemgvv  34634  cplgredgex  35432  acycgrcycl  35458  br8  36067  br6  36068  br4  36069  brsegle  36419  topfne  36675  tailfb  36698  filnetlem1  36699  nndivsub  36778  bj-rest10  37539  isbasisrelowllem1  37810  isbasisrelowllem2  37811  fvineqsnf1  37865  wl-2sb6d  38022  curf  38058  curunc  38062  poimirlem26  38106  mblfinlem2  38118  cnambfre  38128  itgaddnclem2  38139  ftc1anclem1  38153  grpokerinj  38353  rngoisoval  38437  smprngopr  38512  parteq12  39339  ax12eq  39526  ax12el  39527  2llnjN  40152  2lplnj  40205  elpadd0  40394  lauteq  40680  lpolconN  42072  rexrabdioph  43332  tfsnfin  43890  eliunov2  44216  nzss  44854  iotasbc2  44957  or2expropbilem2  47588  elsetpreimafvbi  47958  reuopreuprim  48093  grlicref  48595  cbvmpox2  48919  naryfvalel  49213  line2x  49337  brab2ddw  49411  brab2ddw2  49412