Theorem sylan9bb 518

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  sylan9bbr  519  baibd  548  syl3an9b  1460  nanbi12  1530  elequ12  2167  sbcom2  2213  2sb5rf  2510  2sb6rf  2511  eqeqan12d  2783  eleq12  2859  ceqsrex2v  3626  elabd2  3638  elabgt  3640  sseq12  3972  csbie2df  4406  2ralsng  4646  rexprgf  4663  rextpg  4667  breq12  5115  reusv2lem5  5371  opelopabg  5521  brabg  5522  opelopabgf  5523  opelopab2  5524  rbropapd  5545  poeq12d  5572  soeq12d  5590  freq12d  5628  seeq12d  5631  weeq12d  5648  ralxpf  5830  feq23  6684  f00  6758  fconstg  6763  f1oeq23  6809  f1o00  6854  fnelfp  7171  fnelnfp  7173  isofrlem  7336  f1oiso  7347  riota1a  7387  cbvmpox  7501  caovord  7619  caovord3  7621  f1oweALT  7965  mpof1o2d  8117  oaordex  8539  oaass  8542  odi  8560  findcard2s  9146  unfilem1  9261  tfsnfin2  9316  suppeqfsuppbi  9335  oieu  9497  r1pw  9813  carddomi2  9952  isacn  10024  djudom2  10163  axdc2  10429  alephval2  10553  distrlem4pr  11007  axpre-sup  11150  nn0ind-raph  12692  elpq  12995  xnn0xadd0  13269  elfz  13537  elfzp12  13627  expeq0  14124  leiso  14492  wrd2ind  14756  trcleq12lem  15026  dfrtrclrec2  15091  shftfib  15105  absdvdsb  16328  dvdsabsb  16329  dvdsabseq  16367  unbenlem  16964  isprs  18348  isdrs  18353  pltval  18382  lublecllem  18410  istos  18468  isdlat  18574  znfld  21675  tgss2  23109  isopn2  23154  cnpf2  23372  lmbr  23380  isreg2  23499  fclsrest  24146  qustgplem  24243  ustuqtoplem  24361  xmetec  24556  nmogelb  24838  metdstri  24974  tcphcph  25361  ulmval  26505  2lgslem1a  27517  elmade  28012  bdayle  28071  iscgrg  28743  istrlson  29991  ispthson  30028  isspthson  30029  elwwlks2on  30247  eupth2lem1  30506  eigrei  32123  eigorthi  32126  jplem1  32557  superpos  32643  chrelati  32653  br8d  32890  ellpi  33626  issiga  34443  eulerpartlemgvv  34707  cplgredgex  35508  acycgrcycl  35534  br8  36143  br6  36144  br4  36145  brsegle  36495  topfne  36750  tailfb  36773  filnetlem1  36774  nndivsub  36853  bj-rest10  37613  isbasisrelowllem1  37884  isbasisrelowllem2  37885  fvineqsnf1  37939  wl-2sb6d  38096  curf  38132  curunc  38136  poimirlem26  38180  mblfinlem2  38192  cnambfre  38202  itgaddnclem2  38213  ftc1anclem1  38227  grpokerinj  38427  rngoisoval  38511  smprngopr  38586  parteq12  39413  ax12eq  39600  ax12el  39601  2llnjN  40226  2lplnj  40279  elpadd0  40468  lauteq  40754  lpolconN  42146  rexrabdioph  43406  tfsnfin  43964  eliunov2  44290  nzss  44912  iotasbc2  45015  or2expropbilem2  47652  elsetpreimafvbi  48022  reuopreuprim  48157  grlicref  48659  smprngprmrng  48986  cbvmpox2  48994  naryfvalel  49288  line2x  49412  brab2ddw  49485  brab2ddw2  49486